| 2004 | Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. | In-Ho Moon, Carl Pixley |
| 2004 | Scalable Automated Verification via Expert-System Guided Transformations. | Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman, Andreas Kuehlmann |
| 2004 | Integrating Reasoning About Ordinal Arithmetic into ACL2. | Panagiotis Manolios, Daron Vroon |
| 2004 | Simple Bounded LTL Model Checking. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | Extending Extended Vacuity. | Arie Gurfinkel, Marsha Chechik |
| 2004 | Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. | Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2004 | QuBE++: An Efficient QBF Solver. | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
| 2004 | Bloom Filters in Probabilistic Verification. | Peter C. Dillinger, Panagiotis Manolios |
| 2004 | Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. | Thao Dang, Alexandre Donz, Oded Maler |
| 2004 | An Operational Semantics for Weak PSL. | Koen Claessen, Johan Mrtensson |
| 2004 | Bounded Verification of Past LTL. | Alessandro Cimatti, Marco Roveri, Daniel Sheridan |
| 2004 | A Simple Method for Parameterized Verification of Cache Coherence Protocols. | Ching-Tsun Chou, Phanindra K. Mannava, Seungjoon Park |
| 2004 | Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. | Lubos Brim, Ivana Cern, Pavel Moravec, Jir Simsa |
| 2004 | Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. | Mohammad Awedh, Fabio Somenzi |
| 2004 | Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs. | Laurent Arditi, Grard Berry, Michael Kishinevsky |
| 2004 | A Hybrid of Counterexample-Based and Proof-Based Abstraction. | Nina Amla, Kenneth L. McMillan |
| 2004 | A Methodology for the Formal Verification of FFT Algorithms in HOL. | Behzad Akbarpour, Sofine Tahar |
| 2004 | Synchronization-at-Retirement for Pipeline Verification. | Mark D. Aagaard, Nancy A. Day, Robert B. Jones |
| 2004 | Combining Equivalence Verification and Completion Functions. | Mark D. Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati |
| 2002 | Generalized Symbolic Trajectory Evaluation - Abstraction in Action. | Jin Yang, Carl-Johan H. Seger |
| 2002 | Sharp Disjunctive Decomposition for Language Emptiness Checking. | Chao Wang, Gary D. Hachtel |
| 2002 | On Solving Presburger and Linear Arithmetic with SAT. | Ofer Strichman |
| 2002 | Analysis of Symbolic SCC Hull Algorithms. | Fabio Somenzi, Kavita Ravi, Roderick Bloem |
| 2002 | Traversal Techniques for Concurrent Systems. | Marc Sol, Enric Pastor |
| 2002 | Functional Design Using Behavioural and Structural Components. | Richard Sharp |