| 2002 | A Fixpoint Based Encoding for Bounded Model Checking. Alan M. Frisch, Daniel Sheridan, Toby Walsh |
| 2002 | A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. Prosenjit Chatterjee, Ganesh Gopalakrishnan |
| 2002 | Abstraction by Symbolic Indexing Transformations. Thomas F. Melham, Robert B. Jones |
| 2002 | Analysis of Symbolic SCC Hull Algorithms. Fabio Somenzi, Kavita Ravi, Roderick Bloem |
| 2002 | Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang |
| 2002 | Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries. Steve McKeever, Wayne Luk, Arran Derbyshire |
| 2002 | Counter-Example Based Predicate Discovery in Predicate Abstraction. Satyaki Das, David L. Dill |
| 2002 | Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. Vijay Ganesh, Sergey Berezin, David L. Dill |
| 2002 | Exploiting Transition Locality in the Disk Based Mur phi Verifier. Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli |
| 2002 | Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings Mark D. Aagaard, John W. O'Leary |
| 2002 | Functional Design Using Behavioural and Structural Components. Richard Sharp |
| 2002 | Generalized Symbolic Trajectory Evaluation - Abstraction in Action. Jin Yang, Carl-Johan H. Seger |
| 2002 | Input/Output Compatibility of Reactive Systems. Josep Carmona, Jordi Cortadella |
| 2002 | Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. Jun Sawada, Ruben Gamboa |
| 2002 | Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV. Meine van der Meulen |
| 2002 | Modeling and Verification of Out-of-Order Microprocessors in UCLID. Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant |
| 2002 | On Solving Presburger and Linear Arithmetic with SAT. Ofer Strichman |
| 2002 | QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. Abdelwaheb Ayari, David A. Basin |
| 2002 | Relating Multi-step and Single-Step Microprocessor Correctness Statements. Mark D. Aagaard, Nancy A. Day, Meng Lou |
| 2002 | Sharp Disjunctive Decomposition for Language Emptiness Checking. Chao Wang, Gary D. Hachtel |
| 2002 | Simplifying Circuits for Formal Verification Using Parametric Representation. In-Ho Moon, Hee-Hwan Kwak, James H. Kukula, Thomas R. Shiple, Carl Pixley |
| 2002 | Smart Play-out of Behavioral Requirements. David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
| 2002 | Traversal Techniques for Concurrent Systems. Marc Solé, Enric Pastor |
| 2002 | Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. Gianfranco Ciardo, Radu Siminiceanu |