| 2002 | Applying SAT Methods in Unbounded Symbolic Model Checking. | Kenneth L. McMillan |
| 2002 | Compressing Transitions for Model Checking. | Robert P. Kurshan, Vladimir Levin, Hsn Yenign |
| 2002 | Model Checking Linear Properties of Prefix-Recognizable Systems. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2002 | Canonical Prefixes of Petri Net Unfoldings. | Victor Khomenko, Maciej Koutny, Walter Vogler |
| 2002 | Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving. | Christian Jacobi |
| 2002 | Software Analysis and Model Checking. | Gerard J. Holzmann |
| 2002 | Temporal-Safety Proofs for Systems Code. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grgoire Sutre, Westley Weimer |
| 2002 | The Symbolic Approach to Hybrid Systems. | Thomas A. Henzinger |
| 2002 | On Discrete Modeling and Model Checking for Nonlinear Analog Systems. | Walter Hartong, Lars Hedrich, Erich Barke |
| 2002 | Fair Simulation Minimization. | Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi |
| 2002 | AMC: An Adaptive Model Checker. | Alex Groce, Doron A. Peled, Mihalis Yannakakis |
| 2002 | Automatic Abstraction Using Generalized Model Checking. | Patrice Godefroid, Radha Jagadeesan |
| 2002 | A Modular Checker for Multithreaded Programs. | Cormac Flanagan, Shaz Qadeer, Sanjit A. Seshia |
| 2002 | Abstracting C with abC. | Dennis Dams, William Hesse, Gerard J. Holzmann |
| 2002 | On Abstraction in Software Verification. | Patrick Cousot, Radhia Cousot |
| 2002 | Practical Methods for Proving Program Termination. | Michael Coln, Henny Sipma |
| 2002 | SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. | Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman |
| 2002 | NuSMV 2: An OpenSource Tool for Symbolic Model Checking. | Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
| 2002 | Automated Unbounded Verification of Security Protocols. | Yannick Chevalier, Laurent Vigneron |
| 2002 | chi-Chek: A Multi-valued Model-Checker. | Marsha Chechik, Arie Gurfinkel, Benet Devereux |
| 2002 | Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking. | Prosenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan |
| 2002 | Synchronous and Bidirectional Component Interfaces. | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2002 | Interface Compatibility Checking for Software Modules. | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang |
| 2002 | Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. | Gianpiero Cabodi, Sergio Nocco, Stefano Quer |
| 2002 | Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |