| 2013 | Probabilistic Program Analysis with Martingales. | Aleksandar Chakarov, Sriram Sankaranarayanan |
| 2013 | Combining Relational Learning with SMT Solvers Using CEGAR. | Arun Tejasvi Chaganty, Akash Lal, Aditya V. Nori, Sriram K. Rajamani |
| 2013 | Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
| 2013 | Better Termination Proving through Cooperation. | Marc Brockschmidt, Byron Cook, Carsten Fuhs |
| 2013 | Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. | Lubos Brim, Milan Ceska, Sven Drazan, David Safrnek |
| 2013 | PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games. | Romain Brenguier |
| 2013 | Formal Verification of Hardware Synthesis. | Thomas Braibant, Adam Chlipala |
| 2013 | QUAIL: A Quantitative Security Analyzer for Imperative Code. | Fabrizio Biondi, Axel Legay, Louis-Marie Traonouez, Andrzej Wasowski |
| 2013 | Distributed Explicit State Model Checking of Deadlock Freedom. | Brad D. Bingham, Jesse D. Bingham, John Erickson, Mark R. Greenstreet |
| 2013 | Solving Existentially Quantified Horn Clauses. | Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko |
| 2013 | Ranking Functions for Linear-Constraint Loops. | Amir M. Ben-Amram |
| 2013 | DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. | Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlcek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimr Still, Jir Weiser |
| 2013 | SVA and PSL Local Variables - A Practical Approach. | Roy Armoni, Dana Fisman, Naiyong Jin |
| 2013 | Verification of Imperative Programs through Transformation of Constraint Logic Programs. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2013 | PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. | tienne Andr, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin |
| 2013 | Automatic Generation of Quality Specifications. | Shaull Almagor, Guy Avni, Orna Kupferman |
| 2013 | Partial Orders for Efficient Bounded Model Checking of Concurrent Software. | Jade Alglave, Daniel Kroening, Michael Tautschnig |
| 2013 | Beautiful Interpolants. | Aws Albarghouthi, Kenneth L. McMillan |
| 2013 | Recursive Program Synthesis. | Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid |
| 2013 | Cryptographic Protocol Verification via Supercompilation (A Case Study). | Abdulbasit Ahmed, Alexei Lisitsa, Andrei P. Nemytykh |
| 2013 | Relative Equivalence in the Presence of Ambiguity. | Oshri Adler, Cindy Eisner, Tatyana Veksler |
| 2013 | Learning Universally Quantified Invariants of Linear Data Structures. | Pranav Garg, Christof Lding, P. Madhusudan, Daniel Neider |
| 2012 | Timed Relational Abstractions for Sampled Data Control Systems. | Aditya Zutshi, Sriram Sankaranarayanan, Ashish Tiwari |
| 2012 | The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. | Arnaud Venet |
| 2012 | HybridSAL Relational Abstracter. | Ashish Tiwari |