FMCAD 2006
Formal Methods in Computer Aided Design
San Jose, CA, USA
November 12 - 16
                           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