| 2012 | A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle |
| 2012 | A Complete Method for Symmetry Reduction in Safety Verification. Duc-Hiep Chu, Joxan Jaffar |
| 2012 | A Method for Symbolic Computation of Abstract Operations. Aditya V. Thakur, Thomas W. Reps |
| 2012 | A Model Checker for Hierarchical Probabilistic Real-Time Systems. Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong |
| 2012 | A Solver for Reachability Modulo Theories. Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri |
| 2012 | ACTL ∩ LTL Synthesis. Rüdiger Ehlers |
| 2012 | APEX: An Analyzer for Open Probabilistic Programs. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell |
| 2012 | Acacia+, a Tool for LTL Synthesis. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, Jean-François Raskin |
| 2012 | Alternate and Learn: Finding Witnesses without Looking All over. Nishant Sinha, Nimit Singhania, Satish Chandra, Manu Sridharan |
| 2012 | An Axiomatic Memory Model for POWER Multiprocessors. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams |
| 2012 | Approximately Bisimilar Symbolic Models for Digital Control Systems. Rupak Majumdar, Majid Zamani |
| 2012 | Assume-Guarantee Abstraction Refinement for Probabilistic Systems. Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke |
| 2012 | Automated Termination Proofs for Java Programs with Cyclic Data. Marc Brockschmidt, Richard Musiol, Carsten Otto, Jürgen Giesl |
| 2012 | Automatic Quantification of Cache Side-Channels. Boris Köpf, Laurent Mauborgne, Martín Ochoa |
| 2012 | Bma: Visual Tool for Modeling and Analyzing Biological Networks. David Benqué, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi |
| 2012 | CSolve: Verifying C with Liquid Types. Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala |
| 2012 | Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings P. Madhusudan, Sanjit A. Seshia |
| 2012 | Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. Cyrille Jégourel, Axel Legay, Sean Sedwards |
| 2012 | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi |
| 2012 | Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin |
| 2012 | Detecting Fair Non-termination in Multithreaded Programs. Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal |
| 2012 | Deterministic Automata for the (F, G)-Fragment of LTL. Jan Kretínský, Javier Esparza |
| 2012 | Diagnosing Abstraction Failure for Separation Logic-Based Analyses. Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger |
| 2012 | Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný |
| 2012 | Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas W. Reps, Phillip A. Porras, Hassen Saïdi, Vinod Yegneswaran |
| 2012 | Euler: A System for Numerical Optimization of Programs. Swarat Chaudhuri, Armando Solar-Lezama |
| 2012 | Exercises in Nonstandard Static Analysis of Hybrid Systems. Ichiro Hasuo, Kohei Suenaga |
| 2012 | Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System. Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero, Andrei Tchaltsev |
| 2012 | Formal Verification of Genetic Circuits. Chris J. Myers |
| 2012 | From C to Infinity and Back: Unbounded Auto-active Verification with VCC. Michal Moskal |
| 2012 | Hector: An Equivalence Checker for a Higher-Order Fragment of ML. David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong |
| 2012 | How to Prove Algorithms Linearisable. Gerhard Schellhorn, Heike Wehrheim, John Derrick |
| 2012 | HybridSAL Relational Abstracter. Ashish Tiwari |
| 2012 | IC3 and beyond: Incremental, Inductive Verification. Aaron R. Bradley |
| 2012 | Incremental, Inductive CTL Model Checking. Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2012 | Interpolants as Classifiers. Rahul Sharma, Aditya V. Nori, Alex Aiken |
| 2012 | Joogie: Infeasible Code Detection for Java. Stephan Arlt, Martin Schäf |
| 2012 | Learning Boolean Functions Incrementally. Yu-Fang Chen, Bow-Yaw Wang |
| 2012 | Leveraging Interpolant Strength in Model Checking. Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina |
| 2012 | Lock Removal for Concurrent Trace Programs. Vineet Kahlon, Chao Wang |
| 2012 | MGSyn: Automatic Synthesis for Industrial Automation. Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, Alois C. Knoll |
| 2012 | Minimum Satisfying Assignments for SMT. Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken |
| 2012 | Model Checking Cell Biology. David L. Dill |
| 2012 | On Decidability of Prebisimulation for Timed Automata. Shibashis Guha, Chinmay Narayan, S. Arun-Kumar |
| 2012 | OpenNWA: A Nested-Word Automaton Library. Evan Driscoll, Aditya V. Thakur, Thomas W. Reps |
| 2012 | Proving Termination of Probabilistic Programs Using Patterns. Javier Esparza, Andreas Gaiser, Stefan Kiefer |
| 2012 | Recent Developments in FDR. Philip J. Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell |
| 2012 | Resource Aware ML. Jan Hoffmann, Klaus Aehlig, Martin Hofmann |
| 2012 | SAFARI: SMT-Based Abstraction for Arrays with Interpolants. Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | SPT: Storyboard Programming Tool. Rishabh Singh, Armando Solar-Lezama |
| 2012 | SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo |
| 2012 | Secure Programming via Visibly Pushdown Safety Games. William R. Harris, Somesh Jha, Thomas W. Reps |
| 2012 | Software Model Checking via IC3. Alessandro Cimatti, Alberto Griggio |
| 2012 | Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters. Matthew Hague, Anthony Widjaja Lin |
| 2012 | Synthesis and Some of Its Challenges. Wolfgang Thomas |
| 2012 | Synthesizing Number Transformations from Input-Output Examples. Rishabh Singh, Sumit Gulwani |
| 2012 | Synthesizing Programs with Constraint Solvers. Rastislav Bodík, Emina Torlak |
| 2012 | TRACER: A Symbolic Execution Tool for Verification. Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa |
| 2012 | Termination Analysis with Algorithmic Learning. Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi |
| 2012 | The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. Arnaud Venet |
| 2012 | Timed Relational Abstractions for Sampled Data Control Systems. Aditya Zutshi, Sriram Sankaranarayanan, Ashish Tiwari |
| 2012 | Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik |
| 2012 | When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way. Cheng-Shen Han, Jie-Hong Roland Jiang |
| 2012 | nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces. Flavio M. de Paula, Alan J. Hu, Amir Nahir |
| 2012 | passert: A Tool for Debugging Parallel Programs. Daniel Schwartz-Narbonne, Feng Liu, David I. August, Sharad Malik |