| 2016 | Enforcing Termination of Interprocedural Analysis. | Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler |
| 2016 | Securing a Compiler Transformation. | Chaoqiang Deng, Kedar S. Namjoshi |
| 2016 | Bounded Abstract Interpretation. | Maria Christakis, Valentin Wstholz |
| 2016 | Quantitative Monitor Automata. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2016 | Structure-Sensitive Points-To Analysis for C and C++. | George Balatsouras, Yannis Smaragdakis |
| 2016 | Relational Verification Through Horn Clause Transformation. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2016 | Simulation and Invariance for Weak Consistency. | Jade Alglave |
| 2016 | Automated Verification of Linearization Policies. | Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh |
| 2015 | Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR. | Tachio Terauchi |
| 2015 | Precise Data Flow Analysis in the Presence of Correlated Method Calls. | Marianna Rapoport, Ondrej Lhotk, Frank Tip |
| 2015 | A Simple Abstraction of Arrays and Maps by Program Translation. | David Monniaux, Francesco Alberti |
| 2015 | Effective Soundness-Guided Reflection Analysis. | Yue Li, Tian Tan, Jingling Xue |
| 2015 | Shape Analysis for Unstructured Sharing. | Huisong Li, Xavier Rival, Bor-Yuh Evan Chang |
| 2015 | Static Analysis with Set-Closure in Secrecy. | Woosuk Lee, Hyunsook Hong, Kwangkeun Yi, Jung Hee Cheon |
| 2015 | Refinement Type Inference via Horn Constraint Optimization. | Kodai Hashimoto, Hiroshi Unno |
| 2015 | Synthesizing Heap Manipulations via Integer Linear Programming. | Anshul Garg, Subhajit Roy |
| 2015 | SJS: A Type System for JavaScript with Fixed Object Layout. | Wontae Choi, Satish Chandra, George C. Necula, Koushik Sen |
| 2015 | A Binary Decision Tree Abstract Domain Functor. | Junjie Chen, Patrick Cousot |
| 2015 | Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. | Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening |
| 2015 | Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. | Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, Hongseok Yang |
| 2015 | Safety Verification and Refutation by k-Invariants and k-Induction. | Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel |
| 2015 | A Forward Analysis for Recurrent Sets. | Alexey Bakhirkin, Josh Berdine, Nir Piterman |
| 2015 | Static Analysis of Non-interference in Expressive Low-Level Languages. | Peter Aldous, Matthew Might |
| 2015 | May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. | Elvira Albert, Samir Genaim, Pablo Gordillo |
| 2015 | Parallel Cost Analysis of Distributed Systems. | Elvira Albert, Jess Correas, Einar Broch Johnsen, Guillermo Romn-Dez |