FMCAD 2006
International Conference on Formal Methods in Computer-Aided Design
Sponsored by IEEE, CEDA (Council on Electronic Design Automation)
In cooperation with ACM SIGDA
(Special Interest Group on Design Automation)
http://fmcad.org/2006
CALL FOR PARTICIPATION
November 12-16, 2006, San Jose, California
(Note: ICCAD also takes place in San Jose the previous week, Nov. 5-9)
----------------------------------------------
Early Registration Deadline: October 22, 2006
Hotel Registration Deadline: October 22, 2006
----------------------------------------------
FMCAD 2006 is the sixth in a series of conferences on the theory and
applications of formal methods in hardware and system verification. FMCAD
provides a leading forum to researchers in academia and industry for
presenting and discussing groundbreaking methods, technologies,
theoretical results, and tools for reasoning formally about computing
systems. In addition to the technical program, FMCAD will offer a full
day of tutorials on model checking, theorem proving, decision procedures,
and the application of such methods in industry. FMCAD will also include
a panel on complementing simulation with formal methods and an affiliated
workshop on pre- and post-silicon verification.
Tutorials (Full day, November 12, 2006)
========================================================================
Edmund M. Clarke (Carnegie Mellon University)
Model Checking with SAT
J Strother Moore (University of Texas at Austin)
Theorem Proving in Verification: The ACL2 System
Leonardo de Moura (Microsoft Research)
SMT Solvers: Theory & Practice
Jason Baumgartner (IBM)
Integrating FV Into Main-Stream Verification: The IBM Experience
Invited Talks
========================================================================
Ken McMillan (Cadence Berkeley Labs)
What can the SAT Experience Teach us About Abstraction?
Gerard Holzmann (NASA/JPL Laboratory for Reliable Software)
The Design of a Distributed Model Checking Algorithm for Spin
Amir Pnueli (New York University)
Synthesis of Designs from Property Specifications
Panel
========================================================================
Giving the Gorilla some Brains: How can Formal Complement Simulation?
Moderator Andreas Kuehlmann (Cadence Berkeley Labs)
Invited Robert Jones (Intel)
Presentations Life in the Jungle: Simulation vs. Verification
Wolfgang Roesner (IBM)
Ecological Niche or Survival Gear? - Improving an
Industrial Simulation Methodology with Formal Methods
Panelists Edmund Clarke, Warren Hunt, Robert Jones, Robert Kurshan,
Wolfgang Paul, Carl Pixley, and Wolfgang Roesner
Affiliated Workshop
========================================================================
Pre- and Post-Silicon Verification:
Methods and Research Opportunities
Chair Ganesh Gopalakrishnan (University of Utah)
The workshop features a full day of invited talks from industry
experts describing state-of-the-art techniques and problem areas
for both pre- and post-silicon verification.
Program
========================================================================
Sunday, November 12
8:45-9:00 Welcome and Opening Remarks
9:00-10:30 Edmund M. Clarke
Model Checking with SAT
10:30-11:00 Break
11:00-12:30 J Strother Moore
Theorem Proving in Verification: The ACL2 System
12:30-2:00 Lunch
2:00-3:30 Leonardo de Moura
SMT Solvers: Theory & Practice
3:30-4:00 Break
4:00-5:30 Jason Baumgartner
Integrating FV Into Main-Stream Verification: The IBM Experience
Monday, November 13
8:45-9:00 Welcome and Opening Remarks
Invited Talk
9:00-10:00 Ken McMillan
What can the SAT Experience Teach us About Abstraction?
10:00-10:30 Break
Session 1: Hardware Verification
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
11:00-11:30 Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, and Ziyad Hanna
Post-Reboot Equivalence and Compositional Verification of Hardware
11:30-12:00 Sava Krstic, Jordi Cortadella, Mike Kishinevsky, and John O'Leary
Synchronous Elastic Networks
12:00-2:00 Lunch break
Session 2: SAT-based methods
2:00-2:30 Hyondeuk Kim and Fabio Somenzi
Finite Instantiations for Integer Difference Logic
2:30-3:00 Eric Gregoire, Bertrand Mazure, and Cedric Piette
Tracking MUSes and Strict Inconsistent Covers
3:00-3:15 Hossein Sheini and Karem Sakallah
Ario: A Linear Integer Arithmetic Logic Solver
3:15-3:30 Cameron Brien and Sharad Malik
Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers
Through Visual Analysis
3:30-4:00 Break
Session 3: Software Verification
4:00-4:30 Byron Cook, Daniel Kroening, and Natasha Sharygina
Over-Approximating Boolean Programs with Unbounded Thread Creation
4:30-5:00 Neha Rungta and Eric Mercer
An Improved Distance Heuristic Function for Directed Software
Model Checking
5:00-5:30 Amir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart Theelen,
Mohammad Reza Mousavi, and Sander Stuijk
Liveness and Boundedness of Synchronous Data Flow Graph
5:30-5:45 Johannes Faber and Roland Meyer
Model Checking Data-Dependent Real-Time Properties of the European
Train Control System
6:00-7:00 Business meeting
Tuesday, November 14
Invited Talk
9:00-10:00 Gerard Holzmann
The Design of a Distributed Model Checking Algorithm for Spin
10:00-10:30 Break
Session 1: Model Checking
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
11:00-11:30 Florian Pigorsch, Christoph Scholl, and Stefan Disch
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, and
Quantifier Scheduling
11:30-12:00 Ashish Darbari
Symmetry Reduction for STE Model Checking
12:00-12:30 Shiva Nejati, Mihaela Gheorghiu, and Marsha Chechik
Thorough Checking Revisited
12:30-2:30 Lunch break
Session 2: Invited Panel Presentations
2:30-3:00 Robert Jones
Life in the Jungle: Simulation vs. Verification
3:00-3:30 Wolfgang Roesner
Ecological Niche or Survival Gear? - Improving an
Industrial Simulation Methodology with Formal Methods
3:30-4:00 Break
Session 3: Panel Discussion
Moderator: Andreas Kuehlmann
4:00-5:30 Panelists: Edmund Clarke, Warren Hunt, Robert Jones,
Robert Kurshan, Wolfgang Paul, Carl Pixley, and Wolfgang Roesner
Giving the Gorilla Some Brains: How can Formal Complement Simulation?
6:30-10:00 Conference Banquet
(Held in the Computer History Museum)
Wednesday, November 15
Invited Talk
9:00-10:00 Amir Pnueli
Synthesis of Designs from Property Specifications
10:00-10:30 Break
Session 1: Automata Theoretic Methods
10:30-11:00 Barbara Jobstmann and Roderick Bloem
Optimizations for LTL Synthesis
11:00-11:30 Alessandro Cimatti, Marco Roveri, Simone Semprini, and Stefano Tonetta
From PSL to NBA: A Modular Symbolic Encoding
11:30-12:00 Sagar Chaki and Nishant Sinha
Assume-Guarantee Reasoning for Deadlock
12:00-2:00 Lunch break
Session 2: Theorem Proving
2:00-2:30 Husam Abu-Haimed, David Dill, and Sergey Berezin
A Refinement Method for Validity Checking of Quantified First-Order
Formulas in Hardware Verification
2:30-3:00 Michael Gordon, Warren Hunt, Matt Kaufmann, and James Reynolds
An Integration of HOL and ACL2
3:00-3:30 Jun Sawada and Erik Reeber
ACL2SIX : A Hint Used to Integrate a Theorem Prover and an Automated
Verification Tool
3:30-4:00 Break
Session 3: Testing and Verification Applications
4:00-4: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
4:30-5:00 Namrata Shekhar, Priyank Kalla, M. Brandon Meredith, and Florian Enescu
Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with
Finite Word-Length Operands
5:00-5:15 Ali Habibi, Haja Moinudeen, and Sofiene Tahar
Design for Verification of the PCI-X Bus
5:15-5:30 Abu Nasser Mohammed Abdullah, Behzad Akbarpour, and Sofiene Tahar
Formal Analysis and Verification of an OFDM Modem Design using HOL
5:30-5:45 Julien Schmaltz
A Formal Model of Lower System Layers
Workshop Thursday, November 16
========================================================================
Pre- and Post-Silicon Verification in the Industry:
Methods and Research Opportunities
Chair Ganesh Gopalakrishnan (University of Utah)
Organization
========================================================================
Chairs: Aarti Gupta, NEC Labs America
Panagiotis Manolios, Georgia Tech
Local Arrangements: Jeremy Levitt, Mentor Graphics
Vigyan Singhal, Oski Technology
Panels: Andreas Kuehlmann, Cadence
Tutorials: Leonardo de Moura, Microsoft Research
Webmasters: Sudarshan Srinivasan, Georgia Tech
Daron Vroon, Georgia Tech
Workshops: Ganesh Gopalakrishnan, Univ. Utah
Program Committee
========================================================================
Clark Barrett, New York University, USA
Jason Baumgartner, IBM Corporation, USA
Valeria Bertacco, University of Michigan, USA
Dominique Borrione, Grenoble University, France
Supratik Chakraborty, Indian Institute of Technology Bombay, India
Alessandro Cimatti, Istituto per la Ricerca Scientifica e Tecnologica, Italy
Edmund M. Clarke, Carnegie Mellon University, USA
Leonardo de Moura, Microsoft Research, USA
Rolf Drechsler, University of Bremen, Germany
Malay K. Ganai, NEC Laboratories America, USA
Ganesh Gopalakrishnan, University of Utah, USA
Susanne Graf, VERIMAG, France
Orna Grumberg, Technion - Israel Institute of Technology, Israel
Aarti Gupta, NEC Laboratories America, USA
Alan J. Hu, University of British Columbia, Canada
Warren Hunt, University of Texas, USA
Andreas Kuehlmann, Cadence Laboratories, USA
Panagiotis Manolios, Georgia Institute of Technology, USA
Andy Martin, IBM Research Division, USA
Ken McMillan, Cadence Labs, USA
John O'Leary, Intel Corp., USA
Wolfgang Paul, Saarland University, Germany
Carl Pixley, Synopsys Inc., USA
Amir Pnueli, NYU, USA
Natarajan Shankar, SRI International, USA
Mary Sheeran, Chalmers University of Technology, Sweden
Eli Singerman, Intel Corp., Israel
Vigyan Singhal, Oski Technology, Inc., USA
Anna Slobodova, Intel Corp., USA
Fabio Somenzi, University of Colorado at Boulder, USA
Richard Trefler, University of Waterloo, Canada
Matthew Wilding, Rockwell Collins Inc., USA
Yaron Wolfsthal, IBM, Israel
Formal Methods in Computer Aided Design
San Jose, CA, USA
November 12 - 16