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

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)

Debugging

   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

Panelists

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

Moderator
  
  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)

Synthesis 

   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)