| 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 | A Practical Approach to Coverage in Model Checking. Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi |
| 2001 | A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. Monika Maidl |
| 2001 | AGVI - Automatic Generation, Verification, and Implementation of Security Protocols. Dawn Xiaodong Song, Adrian Perrig, Doantam Phan |
| 2001 | Analysis of Recursive State Machines. Rajeev Alur, Kousha Etessami, Mihalis Yannakakis |
| 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 | Attacking Symbolic State Explosion. Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin |
| 2001 | Automated Inductive Verification of Parameterized Protocols. Abhik Roychoudhury, I. V. Ramakrishnan |
| 2001 | Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala |
| 2001 | Automatic Abstraction for Verification of Timed Circuits and Systems. Hao Zheng, Eric Mercer, Chris J. Myers |
| 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 | Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. Zhe Dang |
| 2001 | BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction. Peer Johannsen |
| 2001 | CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss |
| 2001 | Certifying Model Checkers. Kedar S. Namjoshi |
| 2001 | Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings Gérard Berry, Hubert Comon, Alain Finkel |
| 2001 | Distributed Symbolic Model Checking for µ-Calculus. Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2001 | EASN: Integrating ASN.1 and Model Checking. Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen |
| 2001 | EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. Miroslav N. Velev, Randal E. Bryant |
| 2001 | Efficient Model Checking Via Büchi Tableau Automata. Girish Bhat, Rance Cleaveland, Alex Groce |
| 2001 | Fast LTL to Büchi Automata Translation. Paul Gastin, Denis Oddoux |
| 2001 | Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. Per Bjesse, Tim Leonard, Abdel Mokkedem |
| 2001 | Finite Instantiations in Equivalence Logic with Uninterpreted Functions. Yoav Rodeh, Ofer Strichman |
| 2001 | Formalizing a JVML Verifier for Initialization in a Theorem Prover. Yves Bertot |
| 2001 | ICS: Integrated Canonizer and Solver. Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar |
| 2001 | Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen |
| 2001 | Java Bytecode Verification: An Overview. Xavier Leroy |
| 2001 | Job-Shop Scheduling Using Timed Automata. Yasmina Abdeddaïm, Oded Maler |
| 2001 | Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. Gianpiero Cabodi |
| 2001 | Microarchitecture Verification by Compositional Model Checking. Ranjit Jhala, Kenneth L. McMillan |
| 2001 | Model Checking the World Wide Web. Luca de Alfaro |
| 2001 | Model Checking with Formula-Dependent Abstract Models. Alexander Asteroth, Christel Baier, Ulrich Aßmann |
| 2001 | Parameterized Verification with Automatically Computed Inductive Assertions. Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
| 2001 | Rewriting for Symbolic Execution of State Machine Models. J Strother Moore |
| 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 | SDLcheck: A Model Checking Tool. Vladimir Levin, Hüsnü Yenigün |
| 2001 | Software Documentation and the Verification Process. David Lorge Parnas |
| 2001 | Symmetry and Reduced Symmetry in Model Checking. A. Prasad Sistla, Patrice Godefroid |
| 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 | TReX: A Tool for Reachability Analysis of Complex Systems. Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu |
| 2001 | The SLAM Toolkit. Thomas Ball, Sriram K. Rajamani |
| 2001 | The Temporal Logic Sugar. Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh |
| 2001 | Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2 Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane |
| 2001 | Transformation-Based Verification Using Generalized Retiming. Andreas Kuehlmann, Jason Baumgartner |
| 2001 | Truth/SLC - A Parallel Verification Platform for Concurrent Systems. Martin Leucker, Thomas Noll |
| 2001 | Using Timestamping and History Variables to Verify Sequential Consistency. Tamarah Arons |
| 2001 | Verifying Network Protocol Implementations by Symbolic Refinement Checking. Rajeev Alur, Bow-Yaw Wang |
| 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 |