| 2011 | The Flow-Insensitive Precision of Andersen's Analysis in Practice. | Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, Manu Sridharan |
| 2011 | An Abstraction-Refinement Framework for Trigger Querying. | Guy Avni, Orna Kupferman |
| 2010 | Automatic Verification of Determinism for Structured Parallel Programs. | Martin T. Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar |
| 2010 | Strictness Meets Data Flow. | Tom Schrijvers, Alan Mycroft |
| 2010 | Modelling Metamorphism by Abstract Interpretation. | Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend |
| 2010 | Points-to Analysis as a System of Linear Equations. | Rupesh Nasre, Ramaswamy Govindarajan |
| 2010 | Abstract Interpreters for Free. | Matthew Might |
| 2010 | Statically Inferring Complex Heap, Array, and Numeric Invariants. | Bill McCloskey, Thomas W. Reps, Mooly Sagiv |
| 2010 | Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods. | Nadir Matringe, Arnaldo Vieira Moura, Rachid Rebiha |
| 2010 | Thread-Modular Counterexample-Guided Abstraction Refinement. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2010 | Using Static Analysis in Space: Why Doing so? | David Lesens |
| 2010 | Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. | Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll C. Morgan |
| 2010 | Interprocedural Analysis with Lazy Propagation. | Simon Holm Jensen, Anders Mller, Peter Thiemann |
| 2010 | Verifying a Local Generic Solver in Coq. | Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl |
| 2010 | Size-Change Termination and Transition Invariants. | Matthias Heizmann, Neil D. Jones, Andreas Podelski |
| 2010 | Alternation for Termination. | William R. Harris, Akash Lal, Aditya V. Nori, Sriram K. Rajamani |
| 2010 | Boxes: A Symbolic Abstract Domain of Boxes. | Arie Gurfinkel, Sagar Chaki |
| 2010 | Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework - In Memory of Amir Pnueli. | Benjamin Goldberg |
| 2010 | Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely. | Thomas Martin Gawlitza, Helmut Seidl |
| 2010 | Compositional Bitvector Analysis for Concurrent Programs with Nested Locks. | Azadeh Farzan, Zachary Kincaid |
| 2010 | Static Verification for Code Contracts. | Manuel Fhndrich |
| 2010 | Time of Time. | E. Allen Emerson |
| 2010 | Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2010 | A Shape Analysis for Non-linear Data Structures. | Renato Cherini, Lucas Rearte, Javier O. Blanco |
| 2010 | Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables. | Alexandre Chapoutot |