| 2014 | Proving Nontermination via Safety. | Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | EDD: A Declarative Debugger for Sequential Erlang Programs. | Rafael Caballero, Enrique Martin-Martin, Adrin Riesco, Salvador Tamarit |
| 2014 | Alternating Runtime and Size Complexity Analysis of Integer Programs. | Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jrgen Giesl |
| 2014 | Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic. | Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta |
| 2014 | On the Correctness of a Branch Displacement Algorithm. | Jaap Boender, Claudio Sacerdoti Coen |
| 2014 | Status Report on Software Verification - (Competition Summary SV-COMP 2014). | Dirk Beyer |
| 2014 | CIF 3: Model-Based Engineering of Supervisory Controllers. | D. A. van Beek, Wan J. Fokkink, Dennis Hendriks, Albert T. Hofkamp, Jasen Markovski, Joanna M. van de Mortel-Fronczak, Michel A. Reniers |
| 2014 | Computing Conditional Probabilities in Markovian Models Efficiently. | Christel Baier, Joachim Klein, Sascha Klppelholz, Steffen Mrcker |
| 2014 | Compositional Invariant Generation for Timed Systems. | Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz |
| 2014 | SATMC: A SAT-Based Model Checker for Security-Critical Systems. | Alessandro Armando, Roberto Carbone, Luca Compagna |
| 2014 | Verification of Concurrent Quantum Protocols by Equivalence Checking. | Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan |
| 2014 | VeriMAP: A Tool for Verifying Programs through Transformations. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | Discounting in LTL. | Shaull Almagor, Udi Boker, Orna Kupferman |
| 2014 | Decision Procedures for Flat Array Properties. | Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2014 | SACO: Static Analyzer for Concurrent Objects. | Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gmez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Romn-Dez |
| 2014 | Forward Reachability Computation for Autonomous Max-Plus-Linear Systems. | Dieky Adzkiya, Bart De Schutter, Alessandro Abate |
| 2013 | Efficient Property Preservation Checking of Model Refinements. | Anton Wijs, Luc Engelen |
| 2013 | Asynchronous Multi-core Incremental SAT Solving. | Siert Wieringa, Keijo Heljanko |
| 2013 | Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory. | David H. White, Gerald Lttgen |
| 2013 | CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution). | Philipp Wendler |
| 2013 | Intertwined Forward-Backward Reachability Analysis Using Interpolants. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2013 | LTL Model-Checking for Malware Detection. | Fu Song, Tayssir Touili |
| 2013 | Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). | Jiri Slaby, Jan Strejcek, Marek Trtk |
| 2013 | Strength-Based Decomposition of the Property Bchi Automaton for Faster Model Checking. | Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2013 | Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). | Corneliu Popeea, Andrey Rybalchenko |