| 2000 | A Discrete Strategy Improvement Algorithm for Solving Parity Games. Jens Vöge, Marcin Jurdzinski |
| 2000 | A Proof-Carrying Code Architecture for Java. Christopher Colby, Peter Lee, George C. Necula |
| 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
| 2000 | An Abstraction Algorithm for the Verification of Generalized C-Slow Designs. Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen |
| 2000 | An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. Orna Kupferman, Moshe Y. Vardi |
| 2000 | Are Timed Automata Updatable? Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit |
| 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 | Boolean Satisfiability with Transitivity Constraints. Randal E. Bryant, Miroslav N. Velev |
| 2000 | Bounded Model Construction for Monadic Second-Order Logics. Abdelwaheb Ayari, David A. Basin |
| 2000 | Building Circuits from Relations. James H. Kukula, Thomas R. Shiple |
| 2000 | Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta |
| 2000 | Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings E. Allen Emerson, A. Prasad Sistla |
| 2000 | Counterexample-Guided Abstraction Refinement. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
| 2000 | Decision Procedures for Inductive Boolean Functions Based on Alternating Automata. Abdelwaheb Ayari, David A. Basin, Felix Klaedtke |
| 2000 | Detecting Errors Before Reaching Them. Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | Distributing Timed Model Checking - How the Search Order Matters. Gerd Behrmann, Thomas Hune, Frits W. Vaandrager |
| 2000 | Efficient Algorithms for Model Checking Pushdown Systems. Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon |
| 2000 | Efficient Büchi Automata from LTL Formulae. Fabio Somenzi, Roderick Bloem |
| 2000 | Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. Scott D. Stoller, Leena Unnikrishnan, Yanhong A. Liu |
| 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines. Rajeev Alur, Radu Grosu, Michael McDougall |
| 2000 | FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, Yaron Wolfsthal |
| 2000 | Formal Verification of VLIW Microprocessors with Speculative Execution. 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 | Induction in Compositional Model Checking. Kenneth L. McMillan, Shaz Qadeer, James B. Saxe |
| 2000 | Integrating WS1S with PVS. Sam Owre, Harald Rueß |
| 2000 | Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis. Catherine Meadows |
| 2000 | Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. João Marques-Silva, Karem A. Sakallah |
| 2000 | Invited Tutorial: Verification of Infinite-State and Parameterized Systems. Parosh Aziz Abdulla, Bengt Jonsson |
| 2000 | Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. Amir Pnueli |
| 2000 | Liveness and Acceleration in Parameterized Verification. Amir Pnueli, Elad Shahar |
| 2000 | Mechanical Verification of an Ideal Incremental Michaël Rusinowitch, Sorin Stratulat, Francis Klay |
| 2000 | Model Checking Continuous-Time Markov Chains by Transient Analysis. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen |
| 2000 | Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. Franck Cassez, François Laroussinie |
| 2000 | On the Competeness of Compositional Reasoning. Kedar S. Namjoshi, Richard J. Trefler |
| 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 | Regular Model Checking. Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili |
| 2000 | Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. Aurore Annichini, Eugene Asarin, Ahmed Bouajjani |
| 2000 | Syntactic Program Transformations for Automatic Abstraction. Kedar S. Namjoshi, Robert P. Kurshan |
| 2000 | TAPS: A First-Order Verifier for Cryptographic Protocols. Ernie Cohen |
| 2000 | Temporal-Locig Queries. William Chan |
| 2000 | The STATEMATE Verification Environment - Making It Real. Tom Bienmüller, Werner Damm, Hartmut Wittke |
| 2000 | Tuning SAT Checkers for Bounded Model Checking. Ofer Strichman |
| 2000 | Unfoldings of Unbounded Petri Nets. Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nylén |
| 2000 | VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits. Tomohiro Yoneda |
| 2000 | Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. John M. Rushby |
| 2000 | Verifying Advanced Microarchitectures that Support Speculation and Exceptions. Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas |
| 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 |