FMCAD 2009
Formal Methods in Computer Aided Design
Austin, Texas, USA
November 15 - 18

Final Program

Sunday 15. November, Tutorials and Industrial Experience Day

12:00 - 12:30 Registration

12:30 - 14:30 Tutorials (chair Armin Biere)

  Nikolaj Bjorner, Microsoft.
  Bit-Precise Constraints: Applications and Decision Procedures.

  Moshe Y. Vardi, Rice University.
  Formal Techniques for System-Level Verification.

14:30 - 15:00 Coffee

15:00 - 18:00 Industrial Experience Reports (chair Carl Pixley)

  Michael Theobald, D.E. Shaw.

  John Penix, Google.
  Challenges and Opportunities in
  Deploying Enterprise-Wide Program Analysis Tools.

  Joerg Bormann.
  Complete Functional Verification.

18:30 - 20:30 Reception

Monday 16. November, 1st Conference Day

08:15 - 08:45 Registration

08:45 - 09:00 Opening (chairs Armin Biere, Carl Pixley)

09:00 - 10:30 Session 1 (chair Gianpiero Cabodi)

Model Checking

   Yakir Vizel and Orna Grumberg.
   Interpolation-Sequence Based Model Checking.

   Alessandro Cimatti, Jori Dubrovin, Tommi Junttila and Marco Roveri.
   Structure-Aware Computation of Predicate Abstraction.

   Michael Case, Hari Mony, Jason Baumgartner and Robert Kanzelman.
   Enhanced Verification by Temporal Decomposition.

10:30 - 11:00 Coffee

11:00 - 12:20 Session 2 (chair Daniel Kroening)

Software Verification

   Dirk Beyer, Alessandro Cimatti, Alberto Griggio,
   M. Erkan Keremoglu and Roberto Sebastiani.
   Software Model Checking via Large-Block Encoding.

   Jyotirmoy Deshmukh and E. Allen Emerson.
   Verification of Recursive Methods on Tree-like Data Structures.

   Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer and Jim Holt.
   MCC - A runtime verification tool for MCAPI user applications
   (short paper).

12:20 - 12:30 In Memoriam: Amir Pnueli (chair Moshe Vardi)

12:30 - 14:00 Lunch

14:00 - 15:00 Keynote (chair Armin Biere)

  E. Allen Emerson, University of Texas at Austin.

15:00 - 15:30 Coffee

15:30 - 17:30 Session 3 (chair Cesare Tinelli)

Satisfiability Modulo Theory 

   Leonardo de Moura and Nikolaj Bjorner.
   Generalized and Efficient Array Decision Procedures.

   Sagar Chaki, Arie Gurfinkel and Ofer Strichman.
   Decision Diagrams for Linear Arithmetic.

   Malay Ganai and Franjo Ivancic.
   Efficient Decision Procedure for Non-linear Arithmetic Constraints
   using CORDIC.

   Angelo Brillout, Daniel Kroening and Thomas Wahl.
   Mixed Abstractions for Floating-Point Arithmetic.

18:00 - 19:00 Business Meeting (chair Warren Hunt)

Tuesday 17. November, 2nd Conference Day

08:30 - 09:00 Registration

09:00 - 10:00 Session 4 (chair Alessandro Cimatti)


   Saqib Sohail and Fabio Somenzi.
   Safety First: A Two-Stage Algorithm for LTL Games.

   Roderick Bloem, Karin Greimel, Thomas Henzinger and Barbara Jobstmann.
   Synthesizing Robust Systems.

10:00 - 10:30 Coffee

10:30 - 11:30 Session 5 (chair Alan Hu)

Quantitative Reasoning

   William Denman, Behzad Akbarpour, Sofiene Tahar,
   Mohamed H. Zaki and Lawrence Paulson.
   Automated Formal Verification of Analog Designs using MetiTarski.

   Krishnan Kailas, Viresh Paruthi and Brian Monwai.
   Formal Verification of Correctness and Performance of
   Random Priority-based Arbiters.

11:30 - 12:20 Session 6 (chair Natasha Sharygina)

Assume Guarantee Reasoning

   Zurab Khasidashvili, Gavriel Gavrielov and Tom Melham.
   Assume-Guarantee Validation for STE Properties within an SVA

   He Zhu, Fei He, William N.N. Hung, Xiaoyu Song and Ming Gu.
   Data Mining based Decomposition for Assume-Guarantee Reasoning
   (short paper).

12:20 - 14:00 Lunch

14:00 - 15:30 Session 7 (chair Koen Claessen)

Equivalence Checking

   Jason Baumgartner, Hari Mony, Michael Case, Jun Sawada and Karen Yorav.
   Scalable Conditional Equivalence Checking:
   An Automated Invariant-Generation Based Approach.

   Zurab Khasidashvili, Mahmoud Kinanah and Andrei Voronkov.
   Verifying Equivalence of Memories Using a First Order Logic Theorem

   Zurab Khasidashvili, Daher Kaiss and Doron Bustan.
   A Compositional Theory for Observational Equivalence Checking of

15:30 - 16:00 Coffee

16:00 - 17:30 Semiconductor Panel


  Ken Albin, AMD.
  Alan Carlin, Freescale.
  Velu Durairaj, TI.
  Alan Hunter, ARM.
  Tushar Ringe, Analog Devices.
  Dan Smith, NVIDIA.


  Adnan Aziz, University of Texas at Austin.

19:00 - 22:00 Conference Dinner

Wednesday 18. November, 3rd and Last Conference Day

08:30 - 09:00 Registration

09:00 - 10:00 Keynote (chair Carl Pixley)

  John D. Barton, Intel.

10:00 - 10:30 Coffee

10:30 - 11:50 Session 8 (chair Mukul Prasad)


   Brian Keng and Andreas Veneris.
   Scaling VLSI Design Debugging with Interpolation.

   Robert Koenighofer, Georg Hofferek and Roderick Bloem.
   Debugging Formal Specifications Using Simple Counterstrategies.

   Sandip Ray and Warren Hunt.
   Connecting Pre-silicon and Post-silicon Verification
   (short paper).

11:50 - 14:00 EDA Vendors Lunch Panel


  Harry Foster, Mentor.
  Ziyad Hanna, Jasper.
  Kevin Harrer, Synopsys.
  Axel Scherer, Cadence.

  JL Gray, Verilab.

14:00 - 16:00 Session 9 (chair Anna Slobodova)

Case Studies and Verification in the Large

   Sergey Tverdyshev.
   A Verified Platform for a Gate-Level Electronic Control Unit.

   John O'Leary, Murali Talupur and Mark Tuttle.
   Protocol Verification using Flows: An Industrial Experience.

   Jesse Bingham, Flemming Andersen, John Erickson and Gaurav Singh.
   Industrial Strength Refinement Checking (short paper).

   Tom van den Broek and Julien Schmaltz.
   Towards a Formally Verified Network-on-Chip (short paper).

   Levent Erkok, Magnus Carlsson and Adam Wick.
   Hardware/Software Co-verification of Cryptographic Algorithms using
   Cryptol (short paper).

16:00 - 16:30 Coffee

16:30 - 18:00 Session 10 (chair Roderick Bloem)


   Hai Zhou.
   Retiming and Resynthesis with Sweep are
   Complete for Sequential Transformations.

   Eli Arbel, Oleg Rokhlenko and Karen Yorav.
   SAT-based Synthesis of Clock Gating Functions using 3-valued
   Abstraction (best paper award).

   Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko,
   Jiri Simsa, Satnam Singh and Viktor Vafeiadis.
   Finding Heap-Bounds for Hardware Synthesis.

18:00 - 18:15 Closing (chair Armin Biere)