| 2017 | Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration. | Colas Le Guernic |
| 2017 | Loop Invariants from Counterexamples. | Marius Greitschus, Daniel Dietsch, Andreas Podelski |
| 2017 | Relative Store Fragments for Singleton Abstraction. | Leandro Facchinetti, Zachary Palmer, Scott F. Smith |
| 2017 | Securing the SSA Transform. | Chaoqiang Deng, Kedar S. Namjoshi |
| 2017 | Verifying Array Manipulating Programs by Tiling. | Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat |
| 2017 | Learning Shape Analysis. | Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, Daniel Tarlow |
| 2017 | Abstract Semantic Diffing of Evolving Concurrent Programs. | Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2017 | Combining Forward and Backward Abstract Interpretation of Horn Clauses. | Alexey Bakhirkin, David Monniaux |
| 2017 | Probabilistic Horn Clause Verification. | Aws Albarghouthi |
| 2016 | Making k-Object-Sensitive Pointer Analysis More Precise with Still k-Limiting. | Tian Tan, Yue Li, Jingling Xue |
| 2016 | From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models. | Thibault Suzanne, Antoine Min |
| 2016 | The Julia Static Analyzer for Java. | Fausto Spoto |
| 2016 | Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants. | Pierre Roux, Yuen-Lam Voronin, Sriram Sankaranarayanan |
| 2016 | Abstract Interpretation of Supermodular Games. | Francesco Ranzato |
| 2016 | Completeness in Approximate Transduction. | Mila Dalla Preda, Roberto Giacobazzi, Isabella Mastroeni |
| 2016 | Loopy: Programmable and Formally Verified Loop Transformations. | Kedar S. Namjoshi, Nimit Singhania |
| 2016 | Cell Morphing: From Array Programs to Array-Free Horn Clauses. | David Monniaux, Laure Gonnord |
| 2016 | A Parametric Abstract Domain for Lattice-Valued Regular Expressions. | Jan Midtgaard, Flemming Nielson, Hanne Riis Nielson |
| 2016 | Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. | David Menendez, Santosh Nagarakatte, Aarti Gupta |
| 2016 | On the Linear Ranking Problem for Simple Floating-Point Loops. | Fonenantsoa Maurica, Frdric Mesnard, tienne Payet |
| 2016 | Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. | Kensuke Kojima, Minoru Kinoshita, Kohei Suenaga |
| 2016 | Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs. | Matthieu Journault, Antoine Min |
| 2016 | Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis. | Kihong Heo, Hakjoo Oh, Hongseok Yang |
| 2016 | Flow- and Context-Sensitive Points-To Analysis Using Generalized Points-To Graphs. | Pritam M. Gharat, Uday P. Khedker, Alan Mycroft |
| 2016 | Exploiting Sparsity in Difference-Bound Matrices. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |