| 2002 | Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. | Jun Sawada, Ruben Gamboa |
| 2002 | Exploiting Transition Locality in the Disk Based Mur phi Verifier. | Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli |
| 2002 | Simplifying Circuits for Formal Verification Using Parametric Representation. | In-Ho Moon, Hee-Hwan Kwak, James H. Kukula, Thomas R. Shiple, Carl Pixley |
| 2002 | Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV. | Meine van der Meulen |
| 2002 | Abstraction by Symbolic Indexing Transformations. | Thomas F. Melham, Robert B. Jones |
| 2002 | Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries. | Steve McKeever, Wayne Luk, Arran Derbyshire |
| 2002 | Modeling and Verification of Out-of-Order Microprocessors in UCLID. | Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant |
| 2002 | Smart Play-out of Behavioral Requirements. | David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
| 2002 | Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. | Vijay Ganesh, Sergey Berezin, David L. Dill |
| 2002 | A Fixpoint Based Encoding for Bounded Model Checking. | Alan M. Frisch, Daniel Sheridan, Toby Walsh |
| 2002 | Counter-Example Based Predicate Discovery in Predicate Abstraction. | Satyaki Das, David L. Dill |
| 2002 | Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. | Gianfranco Ciardo, Radu Siminiceanu |
| 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 | A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. | Prosenjit Chatterjee, Ganesh Gopalakrishnan |
| 2002 | Input/Output Compatibility of Reactive Systems. | Josep Carmona, Jordi Cortadella |
| 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 |
| 2000 | Symbolic Simulation with Approximate Values. | Chris Wilson, David L. Dill, Randal E. Bryant |
| 2000 | Visualizing System Factorizations with Behavior Tables. | Alex Tsow, Steven D. Johnson |
| 2000 | Monitor-Based Formal Specification of PCI. | Kanna Shimizu, David L. Dill, Alan J. Hu |
| 2000 | Checking Safety Properties Using Induction and a SAT-Solver. | Mary Sheeran, Satnam Singh, Gunnar Stlmarck |
| 2000 | Hardware Modeling Using Function Encapsulation. | Jun Sawada, Warren A. Hunt Jr. |
| 2000 | A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon | David M. Russinoff |
| 2000 | Sequential Equivalence Checking by Symbolic Simulation. | Gerd Ritter |
| 2000 | Do You Trust Your Model Checker? | Wolfgang Reif, Jrgen Ruf, Gerhard Schellhorn, Tobias Vollmer |