| 2005 | Abstract Interpretation with Alien Expressions and Heap Structures. Bor-Yuh Evan Chang, K. Rustan M. Leino |
| 2005 | Abstraction for Liveness. Amir Pnueli |
| 2005 | An Overview of Semantics for the Validation of Numerical Programs. Matthieu Martel |
| 2005 | Automata as Abstractions. Dennis Dams, Kedar S. Namjoshi |
| 2005 | Checking Herbrand Equalities and Beyond. Markus Müller-Olm, Oliver Rüthing, Helmut Seidl |
| 2005 | Cryptographic Protocol Analysis on Real C Code. Jean Goubault-Larrecq, Fabrice Parrennes |
| 2005 | Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. Stephen F. Siegel |
| 2005 | Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. Paul C. Attie, Hana Chockler |
| 2005 | Generalized Typestate Checking for Data Structure Consistency. Patrick Lam, Viktor Kuncak, Martin C. Rinard |
| 2005 | I/O Efficient Directed Model Checking. Shahid Jabbar, Stefan Edelkamp |
| 2005 | Information Flow Analysis for Java Bytecode. Samir Genaim, Fausto Spoto |
| 2005 | Minimizing Counterexample with Unit Core Extraction and Incremental SAT. Shengyu Shen, Ying Qin, Sikun Li |
| 2005 | Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties. Laura Bozzelli |
| 2005 | Model Checking of Systems Employing Commutative Functions. A. Prasad Sistla, Min Zhou, Xiaodong Wang |
| 2005 | On the Complexity of Error Explanation. Nirman Kumar, Viraj Kumar, Mahesh Viswanathan |
| 2005 | Optimizing Bounded Model Checking for Linear Hybrid Systems. Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen |
| 2005 | Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv |
| 2005 | Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. Patrick Cousot |
| 2005 | Purity and Side Effect Analysis for Java Programs. Alexandru Salcianu, Martin C. Rinard |
| 2005 | Scalable Analysis of Linear Systems Using Mathematical Programming. Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna |
| 2005 | Shape Analysis by Predicate Abstraction. Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2005 | Simple Is Better: Efficient Bounded Model Checking for Past LTL. Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2005 | Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs. Julien Bertrane |
| 2005 | Termination of Polynomial Programs. Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | The Arithmetic-Geometric Progression Abstract Domain. Jérôme Feret |
| 2005 | The Verifying Compiler, a Grand Challenge for Computing Research. C. A. R. Hoare |
| 2005 | Verification of an Error Correcting Code by Abstract Interpretation. Charles Hymans |
| 2005 | Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings Radhia Cousot |
| 2005 | Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement. Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
| 2005 | Weak Automata for the Linear Time µ-Calculus. Martin Lange |