| 2012 | Symbolic Automata: The Toolkit. | Margus Veanes, Nikolaj S. Bjrner |
| 2012 | A Proof Assistant for Alloy Specifications. | Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri |
| 2012 | Zeno: An Automated Prover for Properties of Recursive Data Structures. | William Sonnex, Sophia Drossopoulou, Susan Eisenbach |
| 2012 | Pushdown Model Checking for Malware Detection. | Fu Song, Tayssir Touili |
| 2012 | LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). | Carsten Sinz, Florian Merz, Stephan Falke |
| 2012 | Predicate Analysis with BLAST 2.7 - (Competition Contribution). | Pavel Shved, Mikhail U. Mandrykin, Vadim S. Mutilin |
| 2012 | Compositional Termination Proofs for Multi-threaded Programs. | Corneliu Popeea, Andrey Rybalchenko |
| 2012 | Demonstrating Learning of Register Automata. | Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel, Bengt Jonsson |
| 2012 | CPAchecker with Adjustable Predicate Analysis - (Competition Contribution). | Stefan Lwe, Philipp Wendler |
| 2012 | VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata. | Ondrej Lengl, Jir Simcek, Toms Vojnar |
| 2012 | Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. | Frdric Lang, Radu Mateescu |
| 2012 | Java Memory Model-Aware Model Checking. | Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders |
| 2012 | Modeling and Verification of a Dual Chamber Implantable Pacemaker. | Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam |
| 2012 | A Platform for High Performance Statistical Model Checking - PLASMA. | Cyrille Jgourel, Axel Legay, Sean Sedwards |
| 2012 | Parameterized Synthesis. | Swen Jacobs, Roderick Bloem |
| 2012 | Verifying pCTL Model Checking. | Johannes Hlzl, Tobias Nipkow |
| 2012 | Proving Reachability Using FShell - (Competition Contribution). | Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith |
| 2012 | McScM: A General Framework for the Verification of Communicating Machines. | Alexander Heuner, Tristan Le Gall, Grgoire Sutre |
| 2012 | Quantitative Models for a Not So Dumb Grid. | Holger Hermanns |
| 2012 | The Guardol Language and Verification System. | David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham |
| 2012 | Aspect-Oriented Runtime Monitor Certification. | Kevin W. Hamlen, Micah Jones, Meera Sridhar |
| 2012 | HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). | Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko |
| 2012 | Ramsey-Based Analysis of Parity Automata. | Oliver Friedmann, Martin Lange |
| 2012 | Template-Based Controller Synthesis for Timed Systems. | Bernd Finkbeiner, Hans-Jrg Peter |
| 2012 | Automated Analysis of AODV Using UPPAAL. | Ansgar Fehnker, Rob J. van Glabbeek, Peter Hfner, Annabelle McIver, Marius Portmann, Wee Lum Tan |