| 2013 | A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems. Alexander Linden, Pierre Wolper |
| 2013 | An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, Ahmed Rezine |
| 2013 | An Overview of the mCRL2 Toolset and Its Recent Advances. Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, Tim A. C. Willemse |
| 2013 | Analysis of Boolean Programs. Patrice Godefroid, Mihalis Yannakakis |
| 2013 | AppGuard - Enforcing User Requirements on Android Apps. Michael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei, Philipp von Styp-Rekowsky |
| 2013 | As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. Jean-Francois Kempf, Marius Bozga, Oded Maler |
| 2013 | Asynchronous Multi-core Incremental SAT Solving. Siert Wieringa, Keijo Heljanko |
| 2013 | Automatic Testing of Real-Time Graphics Systems. Robert Nagy, Gerardo Schneider, Aram Timofeitchik |
| 2013 | BULL: A Library for Learning Algorithms of Boolean Functions. Yu-Fang Chen, Bow-Yaw Wang |
| 2013 | CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution). Stefan Löwe |
| 2013 | CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution). Philipp Wendler |
| 2013 | CSeq: A Sequentialization Tool for C - (Competition Contribution). Bernd Fischer, Omar Inverso, Gennaro Parlato |
| 2013 | Deriving Probability Density Functions from Probabilistic Functional Programs. Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo |
| 2013 | Efficient Property Preservation Checking of Model Refinements. Anton Wijs, Luc Engelen |
| 2013 | Encoding Monomorphic and Polymorphic Types. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone |
| 2013 | Equivalence Checking of Quantum Protocols. Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan |
| 2013 | Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors. Ajith K. John, Supratik Chakraborty |
| 2013 | Formula Preprocessing in MUS Extraction. Anton Belov, Matti Järvisalo, João Marques-Silva |
| 2013 | Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution). Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer |
| 2013 | Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory. David H. White, Gerald Lüttgen |
| 2013 | Integer Parameter Synthesis for Timed Automata. Aleksandra Jovanovic, Didier Lime, Olivier H. Roux |
| 2013 | Intertwined Forward-Backward Reachability Analysis Using Interpolants. Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2013 | LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution). Stephan Falke, Florian Merz, Carsten Sinz |
| 2013 | LTL Model Checking of Interval Markov Chains. Michael Benedikt, Rastislav Lenhardt, James Worrell |
| 2013 | LTL Model-Checking for Malware Detection. Fu Song, Tayssir Touili |
| 2013 | Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine |
| 2013 | Model Checking Agent Knowledge in Dynamic Access Control Policies. Masoud Koleini, Eike Ritter, Mark Ryan |
| 2013 | Model Checking Database Applications. Milos Gligoric, Rupak Majumdar |
| 2013 | Model-Checking Iterated Games. Chung-Hao Huang, Sven Schewe, Farn Wang |
| 2013 | On-the-Fly Exact Computation of Bisimilarity Distances. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare |
| 2013 | PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. Radu Mateescu, Gwen Salaün |
| 2013 | PRISM-games: A Model Checker for Stochastic Multi-Player Games. Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis |
| 2013 | Policy Analysis for Self-administrated Role-Based Access Control. Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato |
| 2013 | Polyglot: Systematic Analysis for Multiple Statechart Formalisms. Daniel Balasubramanian, Corina S. Pasareanu, Gabor Karsai, Michael R. Lowry |
| 2013 | Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution). Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar |
| 2013 | Proof Tree Preserving Interpolation. Jürgen Christ, Jochen Hoenicke, Alexander Nutz |
| 2013 | Ramsey vs. Lexicographic Termination Proving. Byron Cook, Abigail See, Florian Zuleger |
| 2013 | Runtime Verification Based on Register Automata. Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos |
| 2013 | Second Competition on Software Verification - (Summary of SV-COMP 2013). Dirk Beyer |
| 2013 | Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking. Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2013 | Structural Counter Abstraction. Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey |
| 2013 | Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). Jiri Slaby, Jan Strejcek, Marek Trtík |
| 2013 | Synthesis from LTL Specifications with Mean-Payoff Objectives. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin |
| 2013 | Synthesis of Circular Compositional Program Proofs via Abduction. Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv |
| 2013 | The MathSAT5 SMT Solver. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani |
| 2013 | The Quest for Minimal Quotients for Probabilistic Automata. Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang |
| 2013 | Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). Corneliu Popeea, Andrey Rybalchenko |
| 2013 | Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings Nir Piterman, Scott A. Smolka |
| 2013 | UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik |
| 2013 | Ultimate Automizer with SMTInterpol - (Competition Contribution). Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski |
| 2013 | Unbounded Model-Checking with Interpolation for Regular Language Constraints. Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte |
| 2013 | Underapproximation of Procedure Summaries for Integer Programs. Pierre Ganty, Radu Iosif, Filip Konecný |
| 2013 | Weighted Pushdown Systems with Indexed Weight Domains. Yasuhiko Minamide |
| 2013 | eVolCheck: Incremental Upgrade Checker for C. Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina |