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

Tuesday 17. November, 2nd Conference Day

08:30 - 09:00 Registration

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

Games

   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
   Environment.

   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
   Prover.

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

15:30 - 16:00 Coffee

16:00 - 17:30 Semiconductor Panel

Panelists

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

Moderator

  Adnan Aziz, University of Texas at Austin.

19:00 - 22:00 Conference Dinner