| 2001 | Rewriting for Symbolic Execution of State Machine Models. | J Strother Moore |
| 2001 | CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. | John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss |
| 2001 | A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. | Monika Maidl |
| 2001 | SDLcheck: A Model Checking Tool. | Vladimir Levin, Hsn Yenign |
| 2001 | Truth/SLC - A Parallel Verification Platform for Concurrent Systems. | Martin Leucker, Thomas Noll |
| 2001 | Java Bytecode Verification: An Overview. | Xavier Leroy |
| 2001 | As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. | Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn |
| 2001 | Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. | Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala |
| 2001 | Transformation-Based Verification Using Generalized Retiming. | Andreas Kuehlmann, Jason Baumgartner |
| 2001 | BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction. | Peer Johannsen |
| 2001 | Microarchitecture Verification by Compositional Model Checking. | Ranjit Jhala, Kenneth L. McMillan |
| 2001 | Distributed Symbolic Model Checking for µ-Calculus. | Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2001 | Fast LTL to Bchi Automata Translation. | Paul Gastin, Denis Oddoux |
| 2001 | ICS: Integrated Canonizer and Solver. | Jean-Christophe Fillitre, Sam Owre, Harald Rue, Natarajan Shankar |
| 2001 | A BDD-Based Model Checker for Recursive Programs. | Javier Esparza, Stefan Schwoon |
| 2001 | A Fast Bisimulation Algorithm. | Agostino Dovier, Carla Piazza, Alberto Policriti |
| 2001 | Attacking Symbolic State Explosion. | Giorgio Delzanno, Jean-Franois Raskin, Laurent Van Begin |
| 2001 | Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. | Zhe Dang |
| 2001 | Iterating Transducers. | Dennis Dams, Yassine Lakhnech, Martin Steffen |
| 2001 | Benefits of Bounded Model Checking at an Industrial Setting. | Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi |
| 2001 | TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems. | Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venier, Daniel Weil, Sergio Yovine |
| 2001 | A Practical Approach to Coverage in Model Checking. | Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi |
| 2001 | Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. | Gianpiero Cabodi |
| 2001 | µCRL: A Toolset for Analysing Algebraic Specifications. | Stefan Blom, Wan J. Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol |
| 2001 | Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. | Per Bjesse, Tim Leonard, Abdel Mokkedem |