FMCAD 2004: Accepted Papers

This is a list of accepted papers, generated automatically based on information supplied by the authors at the time of paper submission. Details of the titles, abstracts, etc., might change in the final version.

A Functional Approach to the Formal Specification of Networks on Chip   Julien Schmaltz and Dominique Borrione

A hybrid of counterexample-based and proof-based abstraction   Nina Amla and Ken McMillan

A Methodology for the Formal Verification of FFT Algorithms in HOL   Behzad Akbarpour and Sofiene Tahar

A Partitioning Methodology for BDD-based Verification   Debashis Sahoo, Subramanian Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson

A Simple Method for Parameterized Verification of Cache Coherence Protocols   Ching-Tsun Chou, Phanindra K. Mannava, Seungjoon Park

Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking   L. Brim, I. Cerna, P. Moravec, J. Simsa

An Operational Semantics for Weak PSL   Koen Claessen and Johan Mårtensson

Approximate Symbolic Model Checking for Incomplete Designs   Tobias Nopper, Christoph Scholl

Bloom Filters in Probabilistic Verification   Peter C. Dillinger and Panagiotis Manolios

Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier   G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli

Bounded Verification of Past LTL   Alessandro Cimatti, Marco Roveri, Daniel Sheridan

Clever circuits and fast multipliers   Mary Sheeran

Combining Equivalence Verification and Completion Functions   Mark Aagaard, Vlad Ciubotariu, Jason Higgins, Farzad Khalvati

Extending Extended Vacuity   Arie Gurfinkel and Marsha Chechik

Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States   Mohammad Awedh and Fabio Somenzi

Integrating Reasoning about Ordinal Arithmetic into ACL2   Panagiotis Manolios and Daron Vroon

Invariant Checking Combining Forward and Backward Traversal   Christian Stangier and Thomas Sidle

Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs   Laurent Arditi, Gerard Berry and Michael Kishinevsky

Memory Efficient All-Solutions SAT Solver and its Application for Reachability Analysis   Orna Grumberg, Assaf Schuster and Avi Yadgar

Non-Miter-Based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders   In-Ho Moon and Carl Pixley

Parameterized Vacuity   Marko Samer Helmut Veith

Proof Styles in Operational Semantics   Sandip Ray and J Strother Moore

QuBE++: an Efficient QBF Solver   Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella

Scalable Automated Verification via Expert-System Guided Transformations   Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman, Andreas Kuehlmann

Simple Bounded LTL Model Checking   Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila

Simple yet efficient improvement of SAT based Bounded Model Checking   Emmanuel Zarpas

Synchronization-at-Retirement for Pipeline Verification   Mark D. Aagaard, Nancy A. Day, Robert B. Jones

Variable Reuse for Efficient Image Computation   Zijiang Yang and Rajeev Alur

Verification of Analog and Mixed-Signal Circuits using Hybrid System Techniques   Thao Dang, Alexandre Donze, Oded Maler