| 2012 | A Bit Too Precise? Bounded Verification of Quantized Digital Filters. Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang |
| 2012 | A Platform for High Performance Statistical Model Checking - PLASMA. Cyrille Jégourel, Axel Legay, Sean Sedwards |
| 2012 | A Proof Assistant for Alloy Specifications. Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri |
| 2012 | Aspect-Oriented Runtime Monitor Certification. Kevin W. Hamlen, Micah Jones, Meera Sridhar |
| 2012 | Automated Analysis of AODV Using UPPAAL. Ansgar Fehnker, Rob J. van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan |
| 2012 | Automatic Verification of Competitive Stochastic Systems. Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis |
| 2012 | Block Abstraction Memoization for CPAchecker - (Competition Contribution). Daniel Wonisch |
| 2012 | Bounded Phase Analysis of Message-Passing Programs. Ahmed Bouajjani, Michael Emmi |
| 2012 | CPAchecker with Adjustable Predicate Analysis - (Competition Contribution). Stefan Löwe, Philipp Wendler |
| 2012 | Competition on Software Verification - (SV-COMP). Dirk Beyer |
| 2012 | Compositional Termination Proofs for Multi-threaded Programs. Corneliu Popeea, Andrey Rybalchenko |
| 2012 | Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution). Lucas C. Cordeiro, Jeremy Morse, Denis A. Nicole, Bernd Fischer |
| 2012 | Counter-Example Guided Fence Insertion under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine |
| 2012 | Coupling and Importance Sampling for Statistical Model Checking. Benoît Barbot, Serge Haddad, Claudine Picaronny |
| 2012 | Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Konecný |
| 2012 | Demonstrating Learning of Register Automata. Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel, Bengt Jonsson |
| 2012 | From Under-Approximations to Over-Approximations and Back. Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik |
| 2012 | HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko |
| 2012 | History-Aware Data Structure Repair Using SAT. Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, Kathryn S. McKinley |
| 2012 | Java Memory Model-Aware Model Checking. Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders |
| 2012 | LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). Carsten Sinz, Florian Merz, Stephan Falke |
| 2012 | LTL to Büchi Automata Translation: Fast and More Deterministic. Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek |
| 2012 | McScM: A General Framework for the Verification of Communicating Machines. Alexander Heußner, Tristan Le Gall, Grégoire Sutre |
| 2012 | Minimal Critical Subsystems for Discrete-Time Markov Models. Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen |
| 2012 | Modeling and Verification of a Dual Chamber Implantable Pacemaker. Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam |
| 2012 | Numeric Bounds Analysis with Conflict-Driven Learning. Vijay Victor D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig |
| 2012 | Parameterized Synthesis. Swen Jacobs, Roderick Bloem |
| 2012 | Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. Frédéric Lang, Radu Mateescu |
| 2012 | Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution). Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar |
| 2012 | Predicate Analysis with BLAST 2.7 - (Competition Contribution). Pavel Shved, Mikhail U. Mandrykin, Vadim S. Mutilin |
| 2012 | Proving Reachability Using FShell - (Competition Contribution). Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith |
| 2012 | Pushdown Model Checking for Malware Detection. Fu Song, Tayssir Touili |
| 2012 | Quantitative Models for a Not So Dumb Grid. Holger Hermanns |
| 2012 | QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification. Hu-Hsi Yeh, Cheng-Yin Wu, Chung-Yang (Ric) Huang |
| 2012 | Ramsey-Based Analysis of Parity Automata. Oliver Friedmann, Martin Lange |
| 2012 | Reachability under Contextual Locking. Rohit Chadha, P. Madhusudan, Mahesh Viswanathan |
| 2012 | Reduction-Based Formal Analysis of BGP Instances. Anduo Wang, Carolyn L. Talcott, Alexander J. T. Gurney, Boon Thau Loo, Andre Scedrov |
| 2012 | SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications. Luís Caires, Hugo Torres Vieira |
| 2012 | Symbolic Automata: The Toolkit. Margus Veanes, Nikolaj S. Bjørner |
| 2012 | TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jirí Srba |
| 2012 | Template-Based Controller Synthesis for Timed Systems. Bernd Finkbeiner, Hans-Jörg Peter |
| 2012 | The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta, Alberto Calvi, Alessandro Cappai, Roberto Carbone, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Gabriel Erzse, Simone Frau, Marius Minea, Sebastian Mödersheim, David von Oheimb, Giancarlo Pellegrino, Serena Elisa Ponta, Marco Rocchetto, Michaël Rusinowitch, Mohammad Torabi Dashti, Mathieu Turuani, Luca Viganò |
| 2012 | The Guardol Language and Verification System. David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham |
| 2012 | Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings Cormac Flanagan, Barbara König |
| 2012 | VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata. Ondrej Lengál, Jirí Simácek, Tomás Vojnar |
| 2012 | Verifying pCTL Model Checking. Johannes Hölzl, Tobias Nipkow |
| 2012 | Wolverine: Battling Bugs with Interpolants - (Competition Contribution). Georg Weissenbacher, Daniel Kroening, Sharad Malik |
| 2012 | Zeno: An Automated Prover for Properties of Recursive Data Structures. William Sonnex, Sophia Drossopoulou, Susan Eisenbach |
| 2012 | satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl |