| 2015 | From Verification to Optimizations. | Rigel Gjomemo, Kedar S. Namjoshi, Phu H. Phung, V. N. Venkatakrishnan, Lenore D. Zuck |
| 2015 | A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. | Khalil Ghorbal, Andrew Sogokon, Andr Platzer |
| 2015 | Abstracting and Counting Synchronizing Processes. | Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng |
| 2015 | Automatic Inference of Heap Properties Exploiting Value Domains. | Pietro Ferrara, Peter Mller, Milos Novcek |
| 2015 | Effective Abstractions for Verification under Relaxed Memory Models. | Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, Eran Yahav |
| 2015 | Abstracting Induction by Extrapolation and Interpolation. | Patrick Cousot |
| 2015 | Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications. | Agostino Cortesi, Pietro Ferrara, Marco Pistoia, Omer Tripp |
| 2015 | Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing. | Maria Christakis, Patrice Godefroid |
| 2015 | An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. | Maria Christakis, Peter Mller, Valentin Wstholz |
| 2015 | Abstraction-Based Computation of Reward Measures for Markov Automata. | Bettina Braitling, Luis Mara Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns |
| 2015 | Property Directed Polyhedral Abstraction. | Nikolaj S. Bjrner, Arie Gurfinkel |
| 2015 | Analysis of Infinite-State Graph Transformation Systems by Cluster Abstraction. | Peter Backes, Jan Reineke |
| 2015 | Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. | Assal Adj, Pierre-Loc Garoche |
| 2014 | Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability. | Chao Wang, Kevin Hoang |
| 2014 | Cascade 2.0. | Wei Wang, Clark W. Barrett, Thomas Wies |
| 2014 | Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes. | Lei Song, Lijun Zhang, Jens Chr. Godskesen |
| 2014 | Modular Synthesis of Sketches Using Models. | Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick, Armando Solar-Lezama |
| 2014 | Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. | Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Kalmer Apinis |
| 2014 | Practical Floating-Point Tests with Integer Code. | Anthony Romano |
| 2014 | Relational Thread-Modular Static Value Analysis by Abstract Interpretation. | Antoine Min |
| 2014 | Policy Iteration-Based Conditional Termination and Ranking Functions. | Damien Mass |
| 2014 | Weakest Precondition Synthesis for Compiler Optimizations. | Nuno P. Lopes, Jos Monteiro |
| 2014 | Synthesis for Polynomial Lasso Programs. | Jan Leike, Ashish Tiwari |
| 2014 | Probabilistic Automata for Safety LTL Specifications. | Dileep Kini, Mahesh Viswanathan |
| 2014 | Message-Passing Algorithms for the Verification of Distributed Protocols. | Log Jezequel, Javier Esparza |