| 2006 | A CLP Method for Compositional and Intermittent Predicate Abstraction. | Joxan Jaffar, Andrew E. Santosa, Razvan Voicu |
| 2006 | Parallel External Directed Model Checking with Linear I/O. | Shahid Jabbar, Stefan Edelkamp |
| 2006 | Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems. | Katia Hristova, Yanhong A. Liu |
| 2006 | Systematic Construction of Abstractions for Model-Checking. | Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2006 | Piecewise FIFO Channels Are Analyzable. | Naghmeh Ghafari, Richard J. Trefler |
| 2006 | A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. | Pierre Ganty, Jean-Franois Raskin, Laurent Van Begin |
| 2006 | Environment Abstraction for Parameterized Verification. | Edmund M. Clarke, Muralidhar Talupur, Helmut Veith |
| 2006 | A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula |
| 2006 | What's Decidable About Arrays? | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2006 | Verification of Well-Formed Communicating Recursive State Machines. | Laura Bozzelli, Salvatore La Torre, Adriano Peron |
| 2006 | Complexity Results on Branching-Time Pushdown Model Checking. | Laura Bozzelli |
| 2006 | A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs. | Jesse D. Bingham, Zvonimir Rakamaric |
| 2006 | Ranking Abstraction of Recursive Programs. | Ittai Balaban, Ariel Cohen, Amir Pnueli |
| 2006 | Combining Shape Analyses by Intersecting Abstractions. | Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham |
| 2005 | Model Checking of Systems Employing Commutative Functions. | A. Prasad Sistla, Min Zhou, Xiaodong Wang |
| 2005 | Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. | Stephen F. Siegel |
| 2005 | Minimizing Counterexample with Unit Core Extraction and Incremental SAT. | ShengYu Shen, Ying Qin, Sikun Li |
| 2005 | Scalable Analysis of Linear Systems Using Mathematical Programming. | Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna |
| 2005 | Purity and Side Effect Analysis for Java Programs. | Alexandru Salcianu, Martin C. Rinard |
| 2005 | Abstraction for Liveness. | Amir Pnueli |
| 2005 | Checking Herbrand Equalities and Beyond. | Markus Mller-Olm, Oliver Rthing, Helmut Seidl |
| 2005 | An Overview of Semantics for the Validation of Numerical Programs. | Matthieu Martel |
| 2005 | Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. | Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv |
| 2005 | Simple Is Better: Efficient Bounded Model Checking for Past LTL. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2005 | Weak Automata for the Linear Time -Calculus. | Martin Lange |