| 2004 | Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions. | Sumit Gulwani, George C. Necula |
| 2004 | A Polynomial-Time Algorithm for Global Value Numbering. | Sumit Gulwani, George C. Necula |
| 2004 | Type Inference Against Races. | Cormac Flanagan, Stephen N. Freund |
| 2004 | Approximating the Algebraic Relational Semantics of Imperative Programs. | Michael Coln |
| 2004 | The Octahedron Abstract Domain. | Robert Claris, Jordi Cortadella |
| 2004 | On Logics of Aliasing. | Marius Bozga, Radu Iosif, Yassine Lakhnech |
| 2004 | The Blast Query Language for Software Verification.. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | Information Flow Analysis in Logical Form. | Torben Amtoft, Anindya Banerjee |
| 2003 | Loop Transformations for Reducing Data Space Requirements of Resource-Constrained Applications. | Priya Unnikrishnan, Guangyu Chen, Mahmut T. Kandemir, Mustafa Karaky, Ibrahim Kolcu |
| 2003 | Continuation-Based Partial Evaluation without Continuations. | Peter Thiemann |
| 2003 | Instantaneous Termination in Pure Esterel. | Olivier Tardieu, Robert de Simone |
| 2003 | Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management. | Ran Shaham, Eran Yahav, Elliot K. Kolodner, Shmuel Sagiv |
| 2003 | Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis. | Thomas W. Reps, Stefan Schwoon, Somesh Jha |
| 2003 | Abstract Interpretation of Programs as Markov Decision Processes. | David Monniaux |
| 2003 | Selective Tail Call Elimination. | Yasuhiko Minamide |
| 2003 | Craig Interpolation and Reachability Analysis. | Kenneth L. McMillan |
| 2003 | Class-Level Modular Analysis for Object Oriented Languages. | Francesco Logozzo |
| 2003 | Type Systems for Distributed Data Sharing. | Ben Liblit, Alex Aiken, Katherine A. Yelick |
| 2003 | Inserting Safe Memory Reuse Commands into ML-Like Programs. | Oukseh Lee, Hongseok Yang, Kwangkeun Yi |
| 2003 | Existential Heap Abstraction Entailment Is Undecidable. | Viktor Kuncak, Martin C. Rinard |
| 2003 | Z-Ranking: Using Statistical Analysis to Counter the Impact of Static Analysis Approximations. | Ted Kremenek, Dawson R. Engler |
| 2003 | Program Development Using Abstract Interpretation (And The Ciao System Preprocessor). | Manuel V. Hermenegildo, Germn Puebla, Francisco Bueno, Pedro Lpez-Garca |
| 2003 | Cartesian Factoring of Polyhedra in Linear Relation Analysis. | Nicolas Halbwachs, David Merchat, Catherine Parent-Vigouroux |
| 2003 | Client-Driven Pointer Analysis. | Samuel Z. Guyer, Calvin Lin |
| 2003 | Typestate Verification: Abstraction Techniques and Complexity Results. | John Field, Deepak Goyal, G. Ramalingam, Eran Yahav |