| 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 | A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. Kavita Ravi, Roderick Bloem, Fabio Somenzi |
| 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 |
| 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 | An Algorithm for Strongly Connected Component Analysis in Roderick Bloem, Harold N. Gabow, Fabio Somenzi |
| 2000 | Applications of Hierarchical Verification in Model Checking. Robert Beers, Rajnish Ghughal, Mark D. Aagaard |
| 2000 | Automated Refinement Checking for Asynchronous Processes. Rajeev Alur, Radu Grosu, Bow-Yaw Wang |
| 2000 | B2M: A Semantic Based Tool for BLIF Hardware Descriptions. David A. Basin, Stefan Friedrich, Sebastian Mödersheim |
| 2000 | Border-Block Triangular Form and Conjunction Schedule in Image Computation. In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
| 2000 | Checking Safety Properties Using Induction and a SAT-Solver. Mary Sheeran, Satnam Singh, Gunnar Stålmarck |
| 2000 | Combining Stream-Based and State-Based Verification Techniques. Nancy A. Day, Mark D. Aagaard, Byron Cook |
| 2000 | Correctness of Pipelined Machines. Panagiotis Manolios |
| 2000 | Do You Trust Your Model Checker? Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn, Tobias Vollmer |
| 2000 | Executable Protocol Specification in ESL. Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang |
| 2000 | Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings Warren A. Hunt Jr., Steven D. Johnson |
| 2000 | Formal Verification of Floating Point Trigonometric Functions. John Harrison |
| 2000 | Hardware Modeling Using Function Encapsulation. Jun Sawada, Warren A. Hunt Jr. |
| 2000 | Model Checking Synchronous Timing Diagrams. Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2000 | Model Reductions and a Case Study. Jin Hou, Eduard Cerny |
| 2000 | Modeling and Parameters Synthesis for an Air Traffic Management System. Adilson Luiz Bonifácio, Arnaldo Vieira Moura |
| 2000 | Monitor-Based Formal Specification of PCI. Kanna Shimizu, David L. Dill, Alan J. Hu |
| 2000 | SAT-Based Image Computation with Application in Reachability Analysis. Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta |
| 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 | Sequential Equivalence Checking by Symbolic Simulation. Gerd Ritter |
| 2000 | Speeding Up Image Computation by Using RTL Information. Christoph Meinel, Christian Stangier |
| 2000 | Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs. Kiyoharu Hamaguchi, Hidekazu Urushihara, Toshinobu Kashiwabara |
| 2000 | Symbolic Simulation with Approximate Values. Chris Wilson, David L. Dill, Randal E. Bryant |
| 2000 | The Semantics of Verilog Using Transition System Combinators. Gordon J. Pace |
| 2000 | Trends in Computing. Mark E. Dean |
| 2000 | Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods. Michael D. Jones, Ganesh Gopalakrishnan |
| 2000 | Visualizing System Factorizations with Behavior Tables. Alex Tsow, Steven D. Johnson |