5. FMCAD 2004: Austin, Texas, USA

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