5. FMCAD 2004: Austin, Texas, USA

• Wayne Wolf:
  Challenges in System-Level Design. 1-5
  Electronic Edition (link) BibTeX
• Mary Sheeran:
  Generating Fast Multipliers Using Clever Circuits. 6-20
  Electronic Edition (link) BibTeX
• Thao Dang, Alexandre Donzé, Oded Maler:
  Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. 21-36
  Electronic Edition (link) BibTeX
• Behzad Akbarpour, Sofiène Tahar:
  A Methodology for the Formal Verification of FFT Algorithms in HOL. 37-51
  Electronic Edition (link) BibTeX
• Julien Schmaltz, Dominique Borrione:
  A Functional Approach to the Formal Specification of Networks on Chip. 52-66
  Electronic Edition (link) BibTeX
• Sandip Ray, J. Strother Moore:
  Proof Styles in Operational Semantics. 67-81
  Electronic Edition (link) BibTeX
• Panagiotis Manolios, Daron Vroon:
  Integrating Reasoning About Ordinal Arithmetic into ACL2. 82-97
  Electronic Edition (link) BibTeX
• Mark Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati:
  Combining Equivalence Verification and Completion Functions. 98-112
  Electronic Edition (link) BibTeX
• Mark Aagaard, Nancy A. Day, Robert B. Jones:
  Synchronization-at-Retirement for Pipeline Verification. 113-127
  Electronic Edition (link) BibTeX
• Laurent Arditi, Gérard Berry, Michael Kishinevsky:
  Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs. 128-143
  Electronic Edition (link) BibTeX
• In-Ho Moon, Carl Pixley:
  Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. 144-158
  Electronic Edition (link) BibTeX
• Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman, Andreas Kuehlmann:
  Scalable Automated Verification via Expert-System Guided Transformations. 159-173
  Electronic Edition (link) BibTeX
• Emmanuel Zarpas:
  Simple Yet Efficient Improvements of SAT Based Bounded Model Checking. 174-185
  Electronic Edition (link) BibTeX
• Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila:
  Simple Bounded LTL Model Checking. 186-200
  Electronic Edition (link) BibTeX
• Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella:
  QuBE++: An Efficient QBF Solver. 201-213
  Electronic Edition (link) BibTeX
• Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli:
  Bounded Probabilistic Model Checking with the Muralpha Verifier. 214-229
  Electronic Edition (link) BibTeX
• Mohammad Awedh, Fabio Somenzi:
  Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. 230-244
  Electronic Edition (link) BibTeX
• Alessandro Cimatti, Marco Roveri, Daniel Sheridan:
  Bounded Verification of Past LTL. 245-259
  Electronic Edition (link) BibTeX
• Nina Amla, Kenneth L. McMillan:
  A Hybrid of Counterexample-Based and Proof-Based Abstraction. 260-274
  Electronic Edition (link) BibTeX
• Orna Grumberg, Assaf Schuster, Avi Yadgar:
  Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. 275-289
  Electronic Edition (link) BibTeX
• Tobias Nopper, Christoph Scholl:
  Approximate Symbolic Model Checking for Incomplete Designs. 290-305
  Electronic Edition (link) BibTeX
• Arie Gurfinkel, Marsha Chechik:
  Extending Extended Vacuity. 306-321
  Electronic Edition (link) BibTeX
• Marko Samer, Helmut Veith:
  Parameterized Vacuity. 322-336
  Electronic Edition (link) BibTeX
• Koen Claessen, Johan Mårtensson:
  An Operational Semantics for Weak PSL. 337-351
  Electronic Edition (link) BibTeX
• Lubos Brim, Ivana Cerná, Pavel Moravec, Jirí Simsa:
  Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. 352-366
  Electronic Edition (link) BibTeX
• Peter C. Dillinger, Panagiotis Manolios:
  Bloom Filters in Probabilistic Verification. 367-381
  Electronic Edition (link) BibTeX
• Ching-Tsun Chou, Phanindra K. Mannava, Seungjoon Park:
  A Simple Method for Parameterized Verification of Cache Coherence Protocols. 382-398
  Electronic Edition (link) BibTeX
• Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson:
  A Partitioning Methodology for BDD-Based Verification. 399-413
  Electronic Edition (link) BibTeX
• Christian Stangier, Thomas Sidle:
  Invariant Checking Combining Forward and Backward Traversal. 414-429
  Electronic Edition (link) BibTeX
• Zijiang Yang, Rajeev Alur:
  Variable Reuse for Efficient Image Computation. 430-444
  Electronic Edition (link) BibTeX