| 2008 | Model Checking for Action Abstraction. | Harald Fecher, Michael Huth |
| 2008 | Approximation Refinement for Interpolation-Based Model Checking. | Vijay Victor D'Silva, Mitra Purandare, Daniel Kroening |
| 2008 | Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? | Rayna Dimitrova, Andreas Podelski |
| 2008 | Abstract Interpretation of Cellular Signalling Networks. | Vincent Danos, Jrme Feret, Walter Fontana, Jean Krivine |
| 2008 | Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions. | Radhia Cousot |
| 2008 | Diagnostic Information for Realizability. | Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev |
| 2008 | Abstract Interpretation of the Physical Inputs of Embedded Programs. | Olivier Bouissou, Matthieu Martel |
| 2008 | An Improved Tight Closure Algorithm for Integer Octagonal Constraints. | Roberto Bagnara, Patricia M. Hill, Enea Zaffanella |
| 2008 | Handling Parameterized Systems with Non-atomic Global Conditions. | Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Ahmed Rezine |
| 2007 | Towards Shape Analysis for Device Drivers. | Hongseok Yang |
| 2007 | The Spotlight Principle. | Bjrn Wachter, Bernd Westphal |
| 2007 | Automata-Theoretic Model Checking Revisited. | Moshe Y. Vardi |
| 2007 | Model Checking Nonblocking MPI Programs. | Stephen F. Siegel |
| 2007 | Constraint Solving for Interpolation. | Andrey Rybalchenko, Viorica Sofronie-Stokkermans |
| 2007 | The Constraint Database Approach to Software Verification. | Peter Z. Revesz |
| 2007 | An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures. | Zvonimir Rakamaric, Jesse D. Bingham, Alan J. Hu |
| 2007 | An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints. | Mathias Pron, Nicolas Halbwachs |
| 2007 | Automated Verification of Shape and Size Properties Via Separation Logic. | Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin |
| 2007 | Symmetry and Completeness in the Analysis of Parameterized Systems. | Kedar S. Namjoshi |
| 2007 | Model Checking Via GammaCFA. | Matthew Might, Benjamin Chambers, Olin Shivers |
| 2007 | Interpolants and Symbolic Model Checking. | Kenneth L. McMillan |
| 2007 | Learning Algorithms and Formal Verification (Invited Tutorial). | P. Madhusudan |
| 2007 | Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes. | Francesco Logozzo |
| 2007 | Constructing Specialized Shape Analyses for Uniform Change. | Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps |
| 2007 | Lattice Automata. | Orna Kupferman, Yoad Lustig |