| 2000 | Model Checking Guided Abstraction and Analysis. | Hassen Sadi |
| 2000 | Flattening Is an Improvement. | James Riely, Jan F. Prins |
| 2000 | Model Checking as Constraint Solving. | Andreas Podelski |
| 2000 | Code Specialization Based on Value Profiles. | Robert Muth, Scott A. Watterson, Saumya K. Debray |
| 2000 | Abstract Interpretation of Probabilistic Semantics. | David Monniaux |
| 2000 | Tree Schemata and Fair Termination. | Laurent Mauborgne |
| 2000 | TVLA: A System for Implementing Static Analyses. | Tal Lev-Ami, Shmuel Sagiv |
| 2000 | Partial Redundancy Elimination on Predicated Code. | Jens Knoop, Jean-Francois Collard, Roy Dz-Ching Ju |
| 2000 | FULLDOC: A Full Reporting Debugger for Optimized Code. | Clara Jaramillo, Rajiv Gupta, Mary Lou Soffa |
| 2000 | Enforcing Design Constraints with Object Logic. | Daniel Jackson |
| 2000 | Abstract Interpretation of Game Properties. | Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, Jean-Franois Raskin |
| 2000 | Efficient Inference of Static Types for Java Bytecode. | Etienne M. Gagnon, Laurie J. Hendren, Guillaume Marceau |
| 2000 | Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C. | Jeffrey S. Foster, Manuel Fhndrich, Alexander Aiken |
| 2000 | Unified Analysis of Array and Object References in Strongly Typed Languages. | Stephen J. Fink, Kathleen Knobe, Vivek Sarkar |
| 2000 | Confidentiality Analysis of Mobile Systems. | Jrme Feret |
| 2000 | Checking Cleanness in Linked Lists. | Nurit Dor, Michael Rodeh, Shmuel Sagiv |
| 2000 | Safety of Strictness Analysis via Term Graph Rewriting. | David Clark, Chris Hankin, Sebastian Hunt |
| 2000 | Deriving Parallel Codes via Invariants. | Wei-Ngan Chin, Siau-Cheng Khoo, Zhenjiang Hu, Masato Takeichi |
| 2000 | A Transformational Approach for Generating Non-linear Invariants. | Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech |
| 2000 | Abstract Interpretation Based Semantics of Sequent Calculi. | Gianluca Amato, Giorgio Levi |
| 1999 | Decomposing Non-redundant Sharing by Complementation. | Enea Zaffanella, Patricia M. Hill, Roberto Bagnara |
| 1999 | Static Analysis of Mega-Programs. | Daniel Weise |
| 1999 | Safety versus Secrecy. | Dennis M. Volpano |
| 1999 | Partial Dead Code Elimination Using Extended Value Graph. | Munehiro Takimoto, Kenichi Harada |
| 1999 | Translating Out of Static Single Assignment Form. | Vugranam C. Sreedhar, Roy Dz-Ching Ju, David M. Gillies, Vatsa Santhanam |