| 2012 | Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. | Tobias Nipkow |
| 2012 | Local Symmetry and Compositional Verification. | Kedar S. Namjoshi, Richard J. Trefler |
| 2012 | Modeling Asynchronous Message Passing for C Programs. | Everett Morse, Nick Vrvilo, Eric Mercer, Jay McCarthy |
| 2012 | Automating Induction with an SMT Solver. | K. Rustan M. Leino |
| 2012 | Sound Non-statistical Clustering of Static Analysis Alarms. | Woosuk Lee, Wonchan Lee, Kwangkeun Yi |
| 2012 | Effective Synthesis of Asynchronous Systems from GR(1) Specifications. | Uri Klein, Nir Piterman, Amir Pnueli |
| 2012 | Alternating Control Flow Reconstruction. | Johannes Kinder, Dmitry Kravchenko |
| 2012 | Software Verification with Liquid Types. | Ranjit Jhala |
| 2012 | Inferring Canonical Register Automata. | Falk Howar, Bernhard Steffen, Bengt Jonsson, Sofia Cassel |
| 2012 | Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. | Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta |
| 2012 | Lazy Synthesis. | Bernd Finkbeiner, Swen Jacobs |
| 2012 | Automatic Inference of Access Permissions. | Pietro Ferrara, Peter Mller |
| 2012 | Synthesizing Efficient Controllers. | Christian von Essen, Barbara Jobstmann |
| 2012 | Splitting via Interpolants. | Evren Ermis, Jochen Hoenicke, Andreas Podelski |
| 2012 | Model Checking Information Flow in Reactive Systems. | Rayna Dimitrova, Bernd Finkbeiner, Mt Kovcs, Markus N. Rabe, Helmut Seidl |
| 2012 | Synthesizing Protocols for Digital Contract Signing. | Krishnendu Chatterjee, Vishwanath Raman |
| 2012 | Crowfoot: A Verifier for Higher-Order Store Programs. | Nathaniel Charlton, Ben Horsfall, Bernhard Reus |
| 2012 | Regression Verification for Multi-threaded Programs. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2012 | On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking. | Dmitry Bugaychenko |
| 2012 | Verification of Gap-Order Constraint Abstractions of Counter Systems. | Laura Bozzelli, Sophie Pinchinat |
| 2012 | Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2012 | On the Termination of Integer Loops. | Amir M. Ben-Amram, Samir Genaim, Abu Naser Masud |
| 2012 | Synchronizability for Verification of Asynchronously Communicating Systems. | Samik Basu, Tevfik Bultan, Meriem Ouederni |
| 2012 | Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. | Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik |
| 2011 | Sets with Cardinality Constraints in Satisfiability Modulo Theories. | Philippe Suter, Robin Steiger, Viktor Kuncak |