FMCAD 2006
Formal Methods in Computer Aided Design
San Jose, CA, USA
November 12 - 16
Sunday, November 12
Conference, Day 1
Tutorials All Day, Chair: Leonardo De Moura
8:45-9:00 Aarti Gupta and
Pete Manolios		 Welcome and Opening Remarks
9:00-10:30 Edmund M. Clarke Model Checking with SAT
[Slides]
10:30-11:00 Break
11:00-12:30 J Strother Moore Theorem Proving in Verification: The ACL2 System
[Slides]
12:30-14:00 Lunch
14:00-15:30 Leonardo de Moura SMT Solvers: Theory & Practice
[Slides]
15:30-16:00 Break
16:00-17:30 Jason Baumgartner Integrating FV Into Main-Stream Verification: The IBM Experience
[Slides]
Monday, November 13
Conference, Day 2
8:45-9:00 Aarti Gupta and
Pete Manolios		 Welcome and Opening Remarks
Invited Talk, Chair Warren Hunt
9:00-10:00 Ken McMillan What Can the SAT Experience Teach Us About Abstraction?
[Slides]
10:00-10:30 Break
Session 1: Hardware Verification, Chair: Richard Trefler
10:30-11:00 Tilman Gloekler,
Jason Baumgartner,
Devi Shanmugam,
Rick Seigler,
Gary Van Huben,
Barinjato Ramanandray,
Hari Mony, and
Paul Roessler		 Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning
[Slides]
11:00-11:30 Zurab Khasidashvili,
Marcelo Skaba,
Daher Kaiss, and
Ziyad Hanna		 Post-Reboot Equivalence and Compositional Verification of Hardware
[Slides]
11:30-12:00 Sava Krstic,
Jordi Cortadella,
Mike Kishinevsky, and
John O'Leary		 Synchronous Elastic Networks
[Slides]
12:00-14:00 Lunch
Session 2: SAT-Based Methods, Chair: Ken McMillan
14:00-14:30 Hyondeuk Kim and
Fabio Somenzi		 Finite Instantiations for Integer Difference Logic
14:30-15:00 Eric Gregoire,
Bertrand Mazure, and
Cedric Piette		 Tracking MUSes and Strict Inconsistent Covers
[Slides]
15:00-15:15 Hossein Sheini and
Karem Sakallah		 Ario: A Linear Integer Arithmetic Logic Solver
15:15-15:30 Cameron Brien and
Sharad Malik		 Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers through Visual Analysis
15:30-16:00 Break
Session 3: Software Verification, Chair: Ganesh Gopalakrishnan
16:00-16:30 Byron Cook,
Daniel Kroening, and
Natasha Sharygina		 Over-Approximating Boolean Programs with Unbounded Thread Creation
[Slides]
16:30-17:00 Neha Rungta and
Eric Mercer		 An Improved Distance Heuristic Function for Directed Software Model Checking
[Slides]
17:00-17:30 Amir Hossein Ghamarian,
Marc Geilen,
Twan Basten,
Bart Theelen,
Mohammad Reza Mousavi, and
Sander Stuijk		 Liveness and Boundedness of Synchronous Data Flow Graph
[Slides]
17:30-17:45 Johannes Faber and
Roland Meyer		 Model Checking Data-Dependent Real-Time Properties of the European Train Control System
[Slides]
18:00-19:00 All Business Meeting
Tuesday, November 14
Conference, Day 3
Invited Talk, Chair: Aarti Gupta
9:00-10:00 Gerard Holzmann The design of a distributed model checking algorithm for Spin
[Slides]
10:00-10:30 Break
Session 1: Model Checking, Chair Jason Baumgartner
10:30-11:00 Xiaofang Chen,
Yu Yang,
Ganesh Gopalakrishnan, and
Ching-Tsun Chou		 Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee
[Slides]
11:00-11:30 Florian Pigorsch,
Christoph Scholl, and
Stefan Disch		 Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, and Quantifier Scheduling
[Slides]
11:30-12:00 Ashish Darbari Symmetry Reduction for STE Model Checking
[Slides]
12:00-12:30 Shiva Nejati,
Mihaela Gheorghiu, and
Marsha Chechik 		Thorough Checking Revisited
[Slides]
12:30-14:30 Lunch
Session 2: Invited Panel Presentations, Meta-Chair: John O'Leary
14:30-15:00 Robert Jones Life in the Jungle: Simulation vs. Verification
15:00-15:30 Wolfgang Roesner Ecological Niche or Survival Gear? - Improving an Industrial Simulation Methodology with Formal Methods
[Slides]
15:30-16:00 Break
Session 3: Panel Discussion, Moderator: Andreas Kuelhmann
16:00-17:30 Warren Hunt [Slides],
Robert Jones,
Robert Kurshan [Slides],
Wolfgang Paul [Slides],
Carl Pixley [Slides], and
Wolfgang Roesner 		Panel:
Giving the Gorilla Some Brains: How Can Formal Complement Simulation?
[Slides]
18:30 Conference Banquet
Location: Computer History Museum
Wednesday, November 15
Conference, Day 4
Invited Talk, Chair: Pete Manolios
9:00-10:00 Amir Pnueli Synthesis of Designs from Property
Specifications
[Slides]
10:00-10:30 Break
Session 1: Automata Theoretic Methods, Chair: Amir Pnueli
10:30-11:00 Barbara Jobstmann and
Roderick Bloem 		Optimizations for LTL Synthesis
[Slides]
11:00-11:30 Alessandro Cimatti,
Marco Roveri,
Simone Semprini, and
Stefano Tonetta		 From PSL to NBA: A Modular Symbolic Encoding
[Slides]
11:30-12:00 Sagar Chaki and
Nishant Sinha		 Assume-Guarantee Reasoning for
Deadlock
[Slides]
12:00-14:00 Lunch
Session 2: Theorem Proving, Chair: Andy Martin
14:00-14:30 Husam Abu-Haimed,
David Dill, and
Sergey Berezin		 A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification
[Slides]
14:30-15:00 Michael Gordon,
Warren Hunt,
Matt Kaufmann, and
James Reynolds		 An Integration of HOL and ACL2
[Slides]
15:00-15:30 Jun Sawada and
Erik Reeber		 ACL2SIX : A Hint used to Integrate a
Theorem Prover and an Automated Verification Tool
[Slides]
15:30-16:00 Break
Session 3: Testing and Verification Applications, Chair: Christian Jacobi
16:00-16:30 Claude Helmstetter,
Florence Maraninchi,
Laurent Maillet-Contoz, and
Matthieu Moy		 Automatic Generation of Schedulings for
Improving the Test Coverage of Systems-on-a-Chip
[Slides]
16:30-17:00 Namrata Shekhar,
Priyank Kalla,
M. Brandon Meredith, and
Florian Enescu		 Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands
[Slides]
17:00-17:15 Ali Habibi,
Haja Moinudeen, and
Sofiene Tahar		 Design for Verification of the PCI-X Bus
17:15-17:30 Abu Nasser Mohammed Abdullah,
Behzad Akbarpour, and
Sofiene Tahar		 Formal Analysis and Verification of an OFDM Modem Design using HOL
17:30-17:45 Julien Schmaltz A Formal Model of Lower System Layers
[Slides]
Thursday, November 16
Conference, Day 5

Workshop:
Pre- and Post-Silicon Verification:
Methods and Research Opportunities

9:00-10:00 Christian Jacobi Formal Verification in Industry -- Current State and Future Directions
[Slides]
10:00-11:00 Roope Kaivola Balancing Formal and Dynamic Techniques in Validation of Industrial Arithmetic Designs
[Slides]
11:00-11:30 Break
11:30-12:30 All Discussion
12:30-14:15 Lunch
14:15-15:15 Viresh Paruthi Sequential Equivalence Checking across Arbitrary Design Transformations: Technologies and Applications
[Slides]
15:15-16:15 Rick Leatherman On Chip Instrumentation as a Verification Tool
[Slides]
16:15-17:00 All Questions and open microphone. Topics of interest include discussion of future research directions, funding opportunities, and the creation of a workshop summary to send to funding agencies.
[Slides]