| 2012 | TRACER: A Symbolic Execution Tool for Verification. | Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa |
| 2012 | Hector: An Equivalence Checker for a Higher-Order Fragment of ML. | David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong |
| 2012 | Exercises in Nonstandard Static Analysis of Hybrid Systems. | Ichiro Hasuo, Kohei Suenaga |
| 2012 | Incremental, Inductive CTL Model Checking. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2012 | Secure Programming via Visibly Pushdown Safety Games. | William R. Harris, Somesh Jha, Thomas W. Reps |
| 2012 | When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way. | Cheng-Shen Han, Jie-Hong Roland Jiang |
| 2012 | Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters. | Matthew Hague, Anthony Widjaja Lin |
| 2012 | On Decidability of Prebisimulation for Timed Automata. | Shibashis Guha, Chinmay Narayan, S. Arun-Kumar |
| 2012 | Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. | Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin |
| 2012 | Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. | Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas W. Reps, Phillip A. Porras, Hassen Sadi, Vinod Yegneswaran |
| 2012 | Proving Termination of Probabilistic Programs Using Patterns. | Javier Esparza, Andreas Gaiser, Stefan Kiefer |
| 2012 | ACTL ∩ LTL Synthesis. | Rdiger Ehlers |
| 2012 | OpenNWA: A Nested-Word Automaton Library. | Evan Driscoll, Aditya V. Thakur, Thomas W. Reps |
| 2012 | Minimum Satisfying Assignments for SMT. | Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken |
| 2012 | Model Checking Cell Biology. | David L. Dill |
| 2012 | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. | Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zadi |
| 2012 | Software Model Checking via IC3. | Alessandro Cimatti, Alberto Griggio |
| 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 | A Complete Method for Symmetry Reduction in Safety Verification. | Duc-Hiep Chu, Joxan Jaffar |
| 2012 | Learning Boolean Functions Incrementally. | Yu-Fang Chen, Bow-Yaw Wang |
| 2012 | MGSyn: Automatic Synthesis for Industrial Automation. | Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, Alois C. Knoll |
| 2012 | Euler: A System for Numerical Optimization of Programs. | Swarat Chaudhuri, Armando Solar-Lezama |
| 2012 | Automated Termination Proofs for Java Programs with Cyclic Data. | Marc Brockschmidt, Richard Musiol, Carsten Otto, Jrgen Giesl |
| 2012 | Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. | Toms Brzdil, Krishnendu Chatterjee, Antonn Kucera, Petr Novotn |
| 2012 | IC3 and beyond: Incremental, Inductive Verification. | Aaron R. Bradley |