| 2004 | A Functional Approach to the Formal Specification of Networks on Chip. Julien Schmaltz, Dominique Borrione |
| 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, Sofiène Tahar |
| 2004 | A Partitioning Methodology for BDD-Based Verification. Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson |
| 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 | An Operational Semantics for Weak PSL. Koen Claessen, Johan Mårtensson |
| 2004 | Approximate Symbolic Model Checking for Incomplete Designs. Tobias Nopper, Christoph Scholl |
| 2004 | Bloom Filters in Probabilistic Verification. Peter C. Dillinger, Panagiotis Manolios |
| 2004 | Bounded Probabilistic Model Checking with the Mur Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli |
| 2004 | Bounded Verification of Past LTL. Alessandro Cimatti, Marco Roveri, Daniel Sheridan |
| 2004 | Challenges in System-Level Design. Wayne H. Wolf |
| 2004 | Combining Equivalence Verification and Completion Functions. Mark D. Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati |
| 2004 | Extending Extended Vacuity. Arie Gurfinkel, Marsha Chechik |
| 2004 | Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings Alan J. Hu, Andrew K. Martin |
| 2004 | Generating Fast Multipliers Using Clever Circuits. Mary Sheeran |
| 2004 | Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. Mohammad Awedh, Fabio Somenzi |
| 2004 | Integrating Reasoning About Ordinal Arithmetic into ACL2. Panagiotis Manolios, Daron Vroon |
| 2004 | Invariant Checking Combining Forward and Backward Traversal. Christian Stangier, Thomas Sidle |
| 2004 | Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs. Laurent Arditi, Gérard Berry, Michael Kishinevsky |
| 2004 | Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2004 | Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. In-Ho Moon, Carl Pixley |
| 2004 | Parameterized Vacuity. Marko Samer, Helmut Veith |
| 2004 | Proof Styles in Operational Semantics. Sandip Ray, J Strother Moore |
| 2004 | QuBE++: An Efficient QBF Solver. Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
| 2004 | Scalable Automated Verification via Expert-System Guided Transformations. Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman, Andreas Kuehlmann |
| 2004 | Simple Bounded LTL Model Checking. Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | Simple Yet Efficient Improvements of SAT Based Bounded Model Checking. Emmanuel Zarpas |
| 2004 | Synchronization-at-Retirement for Pipeline Verification. Mark D. Aagaard, Nancy A. Day, Robert B. Jones |
| 2004 | Variable Reuse for Efficient Image Computation. Zijiang Yang, Rajeev Alur |
| 2004 | Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. Thao Dang, Alexandre Donzé, Oded Maler |