| 2005 | Generalized Typestate Checking for Data Structure Consistency. | Patrick Lam, Viktor Kuncak, Martin C. Rinard |
| 2005 | On the Complexity of Error Explanation. | Nirman Kumar, Viraj Kumar, Mahesh Viswanathan |
| 2005 | I/O Efficient Directed Model Checking. | Shahid Jabbar, Stefan Edelkamp |
| 2005 | Verification of an Error Correcting Code by Abstract Interpretation. | Charles Hymans |
| 2005 | The Verifying Compiler, a Grand Challenge for Computing Research. | C. A. R. Hoare |
| 2005 | Untitled record | Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham |
| 2005 | Cryptographic Protocol Analysis on Real C Code. | Jean Goubault-Larrecq, Fabrice Parrennes |
| 2005 | Information Flow Analysis for Java Bytecode. | Samir Genaim, Fausto Spoto |
| 2005 | The Arithmetic-Geometric Progression Abstract Domain. | Jrme Feret |
| 2005 | Automata as Abstractions. | Dennis Dams, Kedar S. Namjoshi |
| 2005 | Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. | Patrick Cousot |
| 2005 | Abstract Interpretation with Alien Expressions and Heap Structures. | Bor-Yuh Evan Chang, K. Rustan M. Leino |
| 2005 | Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement. | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
| 2005 | Termination of Polynomial Programs. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties. | Laura Bozzelli |
| 2005 | Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs. | Julien Bertrane |
| 2005 | Shape Analysis by Predicate Abstraction. | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2005 | Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. | Paul C. Attie, Hana Chockler |
| 2005 | Optimizing Bounded Model Checking for Linear Hybrid Systems. | Erika brahm, Bernd Becker, Felix Klaedtke, Martin Steffen |
| 2004 | Checking Interval Based Properties for Reactive Systems. | Yu Pei, Qiwen Xu |
| 2004 | Certifying Temporal Properties for Compiled C Programs. | Songtao Xia, James Hook |
| 2004 | Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone. | Reinhard Wilhelm |
| 2004 | History-Dependent Scheduling for Cryptographic Processes. | Vincent Vanackre |
| 2004 | Construction of a Semantic Model for a Typed Assembly Language. | Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu |
| 2004 | On the Expressive Power of Canonical Abstraction. | Shmuel Sagiv |