| 2001 | Efficient Model Checking Via Bchi Tableau Automata. | Girish Bhat, Rance Cleaveland, Alex Groce |
| 2001 | Formalizing a JVML Verifier for Initialization in a Theorem Prover. | Yves Bertot |
| 2001 | The Temporal Logic Sugar. | Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh |
| 2001 | The SLAM Toolkit. | Thomas Ball, Sriram K. Rajamani |
| 2001 | Model Checking with Formula-Dependent Abstract Models. | Alexander Asteroth, Christel Baier, Ulrich Amann |
| 2001 | Parameterized Verification with Automatically Computed Inductive Assertions. | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
| 2001 | Using Timestamping and History Variables to Verify Sequential Consistency. | Tamarah Arons |
| 2001 | TReX: A Tool for Reachability Analysis of Complex Systems. | Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu |
| 2001 | Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2001 | Verifying Network Protocol Implementations by Symbolic Refinement Checking. | Rajeev Alur, Bow-Yaw Wang |
| 2001 | Analysis of Recursive State Machines. | Rajeev Alur, Kousha Etessami, Mihalis Yannakakis |
| 2001 | Model Checking the World Wide Web. | Luca de Alfaro |
| 2001 | Job-Shop Scheduling Using Timed Automata. | Yasmina Abdeddam, Oded Maler |
| 2000 | VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits. | Tomohiro Yoneda |
| 2000 | Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. | Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta |
| 2000 | A Discrete Strategy Improvement Algorithm for Solving Parity Games. | Jens Vge, Marcin Jurdzinski |
| 2000 | Formal Verification of VLIW Microprocessors with Speculative Execution. | Miroslav N. Velev |
| 2000 | Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. | Scott D. Stoller, Leena Unnikrishnan, Yanhong A. Liu |
| 2000 | Efficient Bchi Automata from LTL Formulae. | Fabio Somenzi, Roderick Bloem |
| 2000 | Tuning SAT Checkers for Bounded Model Checking. | Ofer Strichman |
| 2000 | Mechanical Verification of an Ideal Incremental | Michal Rusinowitch, Sorin Stratulat, Francis Klay |
| 2000 | Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. | John M. Rushby |
| 2000 | XMC: A Logic-Programming-Based Verification Toolset. | C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury, V. N. Venkatakrishnan |
| 2000 | Liveness and Acceleration in Parameterized Verification. | Amir Pnueli, Elad Shahar |
| 2000 | Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. | Amir Pnueli |