| 2000 | Integrating WS1S with PVS. | Sam Owre, Harald Rue |
| 2000 | On the Competeness of Compositional Reasoning. | Kedar S. Namjoshi, Richard J. Trefler |
| 2000 | Syntactic Program Transformations for Automatic Abstraction. | Kedar S. Namjoshi, Robert P. Kurshan |
| 2000 | Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis. | Catherine Meadows |
| 2000 | Induction in Compositional Model Checking. | Kenneth L. McMillan, Shaz Qadeer, James B. Saxe |
| 2000 | Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. | Joo Marques-Silva, Karem A. Sakallah |
| 2000 | An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. | Orna Kupferman, Moshe Y. Vardi |
| 2000 | Building Circuits from Relations. | James H. Kukula, Thomas R. Shiple |
| 2000 | Verifying Advanced Microarchitectures that Support Speculation and Exceptions. | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas |
| 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. | Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
| 2000 | PET: An Interactive Software Testing Tool. | Elsa L. Gunter, Robert P. Kurshan, Doron A. Peled |
| 2000 | Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. | Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix |
| 2000 | Efficient Algorithms for Model Checking Pushdown Systems. | Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon |
| 2000 | Automatic Verification of Parameterized Cache Coherence Protocols. | Giorgio Delzanno |
| 2000 | Binary Reachability Analysis of Discrete Pushdown Timed Automata. | Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su |
| 2000 | A Proof-Carrying Code Architecture for Java. | Christopher Colby, Peter Lee, George C. Necula |
| 2000 | TAPS: A First-Order Verifier for Cryptographic Protocols. | Ernie Cohen |
| 2000 | Counterexample-Guided Abstraction Refinement. | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
| 2000 | Temporal-Locig Queries. | William Chan |
| 2000 | Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. | Franck Cassez, Franois Laroussinie |
| 2000 | Boolean Satisfiability with Transitivity Constraints. | Randal E. Bryant, Miroslav N. Velev |
| 2000 | IF: A Validation Environment for Timed Asynchronous Systems. | Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier |
| 2000 | Are Timed Automata Updatable? | Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit |
| 2000 | Regular Model Checking. | Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili |
| 2000 | The STATEMATE Verification Environment - Making It Real. | Tom Bienmller, Werner Damm, Hartmut Wittke |