FMCAD 2004 Final Program

Sunday, November 14 - Invited Tutorials

8:15-9:00 Registration Desk Open
9:00-12:00 The Challenge of SoC Verification
   Ken Albin - Freescale Semiconductor
   Alan Hunter - ARM
   Eric Sherk - IBM
1:30-2:00 Registration Desk Open
2:00-5:00 Specification and Verification of Shared Memory Protocols and Consistency Models
   Ching Tsun Chou - Intel Corporation
   Steven German - IBM T.J. Watson Research Center
   Ganesh Gopalakrishnan - University of Utah
6:00-9:00 FMCAD Welcome Reception
      -- snacks, drinks, meet-up with people before dinner
      -- Registration Desk Open

Monday, November 15

8:15-9:00 Light Continental Breakfast -- Registration Desk Open
9:00-10:30 Session 1: Circuits
   Session Chair: John O'Leary
Clever circuits and fast multipliers
  Mary Sheeran
Verification of Analog and Mixed-Signal Circuits using Hybrid System Techniques
  Thao Dang, Alexandre Donze, Oded Maler
A Methodology for the Formal Verification of FFT Algorithms in HOL
  Behzad Akbarpour and Sofiene Tahar
10:30-11:00 Break
11:00-12:30 Session 2: Deductive Verification
   Session Chair: Nancy Day
A Functional Approach to the Formal Specification of Networks on Chip
  Julien Schmaltz and Dominique Borrione
Proof Styles in Operational Semantics
  Sandip Ray and J Strother Moore
Integrating Reasoning about Ordinal Arithmetic into ACL2
  Panagiotis Manolios and Daron Vroon
12:30-2:00 Lunch
2:00-3:30 Session 3: Verifying Pipelines
   Session Chair: Ravi Hosabettu
Combining Equivalence Verification and Completion Functions
  Mark Aagaard, Vlad Ciubotariu, Jason Higgins, Farzad Khalvati
Synchronization-at-Retirement for Pipeline Verification
  Mark D. Aagaard, Nancy A. Day, Robert B. Jones
Parameterized Vacuity
  Marko Samer Helmut Veith
  (Moved from Session 10 because of travel schedule problems.)
3:30-4:00 Break
4:00-5:30 Session 4: Hardware Implementation Verification
   Session Chair: Ganesh Gopalakrishnan
Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs
  Laurent Arditi, Gerard Berry and Michael Kishinevsky
Non-Miter-Based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders
  In-Ho Moon and Carl Pixley
Scalable Automated Verification via Expert-System Guided Transformations
  Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman, Andreas Kuehlmann

Tuesday, November 16

8:15-9:00 Light Continental Breakfast -- Registration Desk Open
9:00-10:30 Session 5: Invited Talk -- Wayne Wolf, Princeton University
10:30-11:00 Break
11:00-12:30 Session 6: SAT-Based Model Checking and QBF
   Session Chair: Nina Amla
Simple yet efficient improvement of SAT based Bounded Model Checking
  Emmanuel Zarpas
Simple Bounded LTL Model Checking
  Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila
QuBE++: an Efficient QBF Solver
  Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella
12:30-2:00 Lunch
2:00-3:30 Session 7: Bounded Model Checking
   Session Chair: Robert Jones
Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier
  G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, M. Venturini Zilli
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States
  Mohammad Awedh and Fabio Somenzi
Bounded Verification of Past LTL
  Alessandro Cimatti, Marco Roveri, Daniel Sheridan
3:30-4:00 Break
4:00-5:30 Session 8: Unbounded Model Checking
   Session Chair: Rajeev Alur
A hybrid of counterexample-based and proof-based abstraction
  Nina Amla and Ken McMillan
Memory Efficient All-Solutions SAT Solver and its Application for Reachability Analysis
  Orna Grumberg, Assaf Schuster and Avi Yadgar
Approximate Symbolic Model Checking for Incomplete Designs
  Tobias Nopper, Christoph Scholl
Brief FMCAD business meeting after last session.
5:45-  Banquet

The banquet will be held at Mercury Hall, a restored and converted, turn-of-the century frontier church, with catering by Word of Mouth Catering, rated one of the ten "Best Wedding Caterers" in the US by Bon Appetit magazine.

First bus leaves at 5:45pm.

Second bus leaves after the business meeting.

Wednesday, November 17

8:15-9:00 Light Continental Breakfast -- Registration Desk Open
9:00-10:30 Session 9: Invited Talk -- Greg Spirakis, Intel Corporation
10:30-11:00 Break
11:00-12:00 Session 10: Temporal Logic Specifications
   Session Chair: Ching-Tsun Chou
Extending Extended Vacuity
  Arie Gurfinkel and Marsha Chechik
An Operational Semantics for Weak PSL
  Koen Claessen and Johan Mårtensson
("Parameterized Vacuity" by Samer and Veith moved to Session 3 because of travel scheduling problems.)
12:00-2:00 Lunch
2:00-3:30 Session 11: Explicit State Model Checking
   Session Chair: Enrico Tronci
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking
  L. Brim, I. Cerna, P. Moravec, J. Simsa
Bloom Filters in Probabilistic Verification
  Peter C. Dillinger and Panagiotis Manolios
A Simple Method for Parameterized Verification of Cache Coherence Protocols
  Ching-Tsun Chou, Phanindra K. Mannava, Seungjoon Park
3:30-4:00 Break
4:00-5:30 Session 12: BDD Techniques
   Session Chair: Anna Slobodova
A Partitioning Methodology for BDD-based Verification
  Debashis Sahoo, Subramanian Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson
Invariant Checking Combining Forward and Backward Traversal
  Christian Stangier and Thomas Sidle
Variable Reuse for Efficient Image Computation
  Zijiang Yang and Rajeev Alur