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