| 2012 | Synthesis and Some of Its Challenges. | Wolfgang Thomas |
| 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 | Alternate and Learn: Finding Witnesses without Looking All over. | Nishant Sinha, Nimit Singhania, Satish Chandra, Manu Sridharan |
| 2012 | SPT: Storyboard Programming Tool. | Rishabh Singh, Armando Solar-Lezama |
| 2012 | Synthesizing Number Transformations from Input-Output Examples. | Rishabh Singh, Sumit Gulwani |
| 2012 | Interpolants as Classifiers. | Rahul Sharma, Aditya V. Nori, Alex Aiken |
| 2012 | passert: A Tool for Debugging Parallel Programs. | Daniel Schwartz-Narbonne, Feng Liu, David I. August, Sharad Malik |
| 2012 | How to Prove Algorithms Linearisable. | Gerhard Schellhorn, Heike Wehrheim, John Derrick |
| 2012 | CSolve: Verifying C with Liquid Types. | Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala |
| 2012 | Leveraging Interpolant Strength in Model Checking. | Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina |
| 2012 | nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces. | Flavio M. de Paula, Alan J. Hu, Amir Nahir |
| 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 | Approximately Bisimilar Symbolic Models for Digital Control Systems. | Rupak Majumdar, Majid Zamani |
| 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 | Termination Analysis with Algorithmic Learning. | Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi |
| 2012 | A Solver for Reachability Modulo Theories. | Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri |
| 2012 | SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. | Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Reblo |
| 2012 | Deterministic Automata for the (F, G)-Fragment of LTL. | Jan Kretnsk, Javier Esparza |
| 2012 | Automatic Quantification of Cache Side-Channels. | Boris Kpf, Laurent Mauborgne, Martn Ochoa |
| 2012 | Assume-Guarantee Abstraction Refinement for Probabilistic Systems. | Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke |
| 2012 | APEX: An Analyzer for Open Probabilistic Programs. | Stefan Kiefer, Andrzej S. Murawski, Jol Ouaknine, Bjrn Wachter, James Worrell |
| 2012 | Lock Removal for Concurrent Trace Programs. | Vineet Kahlon, Chao Wang |
| 2012 | Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. | Cyrille Jgourel, Axel Legay, Sean Sedwards |