| 2000 | A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. | Kavita Ravi, Roderick Bloem, Fabio Somenzi |
| 2000 | The Semantics of Verilog Using Transition System Combinators. | Gordon J. Pace |
| 2000 | Border-Block Triangular Form and Conjunction Schedule in Image Computation. | In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
| 2000 | Speeding Up Image Computation by Using RTL Information. | Christoph Meinel, Christian Stangier |
| 2000 | Correctness of Pipelined Machines. | Panagiotis Manolios |
| 2000 | Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods. | Michael D. Jones, Ganesh Gopalakrishnan |
| 2000 | Model Reductions and a Case Study. | Jin Hou, Eduard Cerny |
| 2000 | Formal Verification of Floating Point Trigonometric Functions. | John Harrison |
| 2000 | Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs. | Kiyoharu Hamaguchi, Hidekazu Urushihara, Toshinobu Kashiwabara |
| 2000 | SAT-Based Image Computation with Application in Reachability Analysis. | Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta |
| 2000 | Trends in Computing. | Mark E. Dean |
| 2000 | Combining Stream-Based and State-Based Verification Techniques. | Nancy A. Day, Mark D. Aagaard, Byron Cook |
| 2000 | Executable Protocol Specification in ESL. | Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang |
| 2000 | A Methodology for the Formal Analysis of Asynchronous Micropipelines. | Antonio Cerone, George J. Milne |
| 2000 | A Theory of Consistency for Modular Synchronous Systems. | Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel |
| 2000 | Modeling and Parameters Synthesis for an Air Traffic Management System. | Adilson Luiz Bonifcio, Arnaldo Vieira Moura |
| 2000 | An Algorithm for Strongly Connected Component Analysis in | Roderick Bloem, Harold N. Gabow, Fabio Somenzi |
| 2000 | SAT-Based Verification without State Space Traversal. | Per Bjesse, Koen Claessen |
| 2000 | Scalable Distributed On-the-Fly Symbolic Model Checking. | Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster |
| 2000 | Applications of Hierarchical Verification in Model Checking. | Robert Beers, Rajnish Ghughal, Mark D. Aagaard |
| 2000 | B2M: A Semantic Based Tool for BLIF Hardware Descriptions. | David A. Basin, Stefan Friedrich, Sebastian Mdersheim |
| 2000 | Model Checking Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2000 | Automated Refinement Checking for Asynchronous Processes. | Rajeev Alur, Radu Grosu, Bow-Yaw Wang |
| 2000 | A Methodology for Large-Scale Hardware Verification. | Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger |
| 1998 | A Performance Study of BDD-Based Model Checking. | Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi |