| 2013 | Automatic Synthesis of Deterministic Concurrency. | Veselin Raychev, Martin T. Vechev, Eran Yahav |
| 2013 | Symbolic Automata for Static Specification Mining. | Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang |
| 2013 | Abstract Semantic Differencing for Numerical Programs. | Nimrod Partush, Eran Yahav |
| 2013 | Witnessing Program Transformations. | Kedar S. Namjoshi, Lenore D. Zuck |
| 2013 | Static Provenance Verification for Message Passing Programs. | Rupak Majumdar, Roland Meyer, Zilong Wang |
| 2013 | Contextual Locking for Dynamic Pushdown Networks. | Peter Lammich, Markus Mller-Olm, Helmut Seidl, Alexander Wenner |
| 2013 | Precise Slicing in Imperative Programs via Term-Rewriting and Abstract Interpretation. | Raghavan Komondoor |
| 2013 | Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing. | Hyunha Kim, Kyung-Goo Doh, David A. Schmidt |
| 2013 | Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT. | Eric Goubault |
| 2013 | Abstract Interpretation over Non-lattice Abstract Domains. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2013 | Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. | Alexis Fouilh, David Monniaux, Michal Prin |
| 2013 | Byte-Precise Verification of Low-Level List Manipulation. | Kamil Dudka, Petr Peringer, Toms Vojnar |
| 2013 | Local Shape Analysis for Overlaid Data Structures. | Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2013 | Automatic Verification of Erlang-Style Concurrency. | Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong |
| 2013 | Predicate Abstraction for Relaxed Memory Models. | Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, Eran Yahav |
| 2013 | Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. | Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening |
| 2013 | Formal Verification of a C Value Analysis Based on Abstract Interpretation. | Sandrine Blazy, Vincent Laporte, Andr Maroneze, David Pichardie |
| 2013 | On Solving Universally Quantified Horn Clauses. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2013 | Localizing Widening and Narrowing. | Gianluca Amato, Francesca Scozzari |
| 2013 | Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists. | Pranav Garg, P. Madhusudan, Gennaro Parlato |
| 2013 | Verification as Learning Geometric Concepts. | Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Aditya V. Nori |
| 2012 | A Generalization of Stlmarck's Method. | Aditya V. Thakur, Thomas W. Reps |
| 2012 | Bilateral Algorithms for Symbolic Abstraction. | Aditya V. Thakur, Matt Elder, Thomas W. Reps |
| 2012 | Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version). | Alejandro Snchez, Sriram Sankaranarayanan, Csar Snchez, Bor-Yuh Evan Chang |
| 2012 | A Structural Soundness Proof for Shivers's Escape Technique - A Case for Galois Connections. | Jan Midtgaard, Michael D. Adams, Matthew Might |