| 2000 | Distributing Timed Model Checking - How the Search Order Matters. | Gerd Behrmann, Thomas Hune, Frits W. Vaandrager |
| 2000 | An Abstraction Algorithm for the Verification of Generalized C-Slow Designs. | Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen |
| 2000 | Model Checking Continuous-Time Markov Chains by Transient Analysis. | Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen |
| 2000 | Decision Procedures for Inductive Boolean Functions Based on Alternating Automata. | Abdelwaheb Ayari, David A. Basin, Felix Klaedtke |
| 2000 | Bounded Model Construction for Monadic Second-Order Logics. | Abdelwaheb Ayari, David A. Basin |
| 2000 | Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. | Aurore Annichini, Eugene Asarin, Ahmed Bouajjani |
| 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines. | Rajeev Alur, Radu Grosu, Michael McDougall |
| 2000 | Detecting Errors Before Reaching Them. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | Invited Tutorial: Verification of Infinite-State and Parameterized Systems. | Parosh Aziz Abdulla, Bengt Jonsson |
| 2000 | Unfoldings of Unbounded Petri Nets. | Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nyln |
| 2000 | FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. | Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, Yaron Wolfsthal |
| 1999 | Optimizing Symbolic Model Checking for Constraint-Rich Models. | Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron |
| 1999 | Automatic Verification of Abstract State Machines. | Marc Spielmann |
| 1999 | The Compositional Specification of Timed Systems - A Tutorial. | Joseph Sifakis |
| 1999 | PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. | Johann Schumann |
| 1999 | Abstract and Model Check While You Prove. | Hassen Sadi, Natarajan Shankar |
| 1999 | Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study. | S. Ramesh, Purandar Bhaduri |
| 1999 | Deciding Equality Formulas by Small Domains Instantiations. | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
| 1999 | Efficient Analysis of Cyclic Definitions. | Kedar S. Namjoshi, Robert P. Kurshan |
| 1999 | Elementary Microarchitecture Algebra. | John Matthews, John Launchbury |
| 1999 | Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. | Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers |
| 1999 | Verification of Parameterized Systems by Dynamic Induction on Diagrams. | Zohar Manna, Henny Sipma |
| 1999 | Stepwise CTL Model Checking of State/Event Systems. | Jrn Lind-Nielsen, Henrik Reif Andersen |
| 1999 | A Complete Finite Prefix for Process Algebra. | Rom Langerak, Ed Brinksma |
| 1999 | Model Checking of Safety Properties. | Orna Kupferman, Moshe Y. Vardi |