FMCAD 2007
Formal Methods in Computer Aided Design
Austin, TX, USA
November 11 - 14

Note: All events are in the Trinity Room of the Renaissance Austin Hotel unless stated otherwise.

Sunday, November 11
Conference, Day 1
Tutorials Day, Chair: Natasha Sharygina (University of Lugano)
8:15-8:45 Breakfast
8:45-9:00 Jason Baumgartner
and Mary Sheeran
Welcome and Opening Remarks
9:00-10:00 Robert Brayton The Synergy between Logic Synthesis and Equivalence Checking
10:00-10:30 Break
10:30-12:00 Farid Najm Power Management for VLSI Circuits and the Need for High-Level Power Modeling and Design Exploration
12:00-13:30 Lunch
Location: Arbor Room (Renaissance Austin Hotel)
13:30-15:00 Niklas Een Practical SAT
15:00-15:30 Break
15:30-17:00 Randal E. Bryant Modeling Data in Formal Verification: Bits, Bit Vectors, or Words
17:00-17:30 Break
Panel Discussion, Moderator: Aarti Gupta (NEC)
17:30-19:00 Robert Kurshan,
Hillel Miller,
Rajeev Ranjan,
Harry Foster,
Husam Abu-Haimed,
Prakash Narain
Formal Verification: A Business Perspective
[slides: Gupta, Kurshan, Ranjan, Foster, Abu-Haimed, Narain]
19:00 Reception
Location: Sabine Room (Renaissance Austin Hotel)
Monday, November 12
Conference, Day 2
8:15-9:00 Breakfast
Invited Talk, Chair: Alan Hu (University of British Columbia)
9:00-10:00 Eli Singerman Verification of Embedded Software in Industrial Microprocessors
10:00-10:30 Break
Session 1: SAT-Based Methods, Chair: Miroslav Velev (Consultant)
10:30-11:00 Jocelyn Simmonds,
Jessica Davies,
Arie Gurfinkel, and
Marsha Chechik
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC
11:00-11:30 Sean Safarpour,
Mark Liffiton,
Hratch Mangassarian,
Andreas Veneris, and
Karem Sakallah
Improved Design Debugging using Maximum Satisfiability
11:30-12:00 Daher Kaiss,
Marcelo Skaba,
Ziyad Hanna, and
Zurab Khasidashvili
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification
12:00-12:30 Frank Hutter,
Domagoj Babic,
Holger Hoos, and
Alan Hu
Boosting Verification by Automatic Tuning of Decision Procedures
12:30-14:00 Lunch
Location: Arbor Room (Renaissance Austin Hotel)
Session 2: High-Level System Analysis, Chair: Alper Sen (Freescale)
14:00-14:30 Ariel Cohen,
John O'Leary,
Amir Pnueli,
Mark Tuttle, and
Lenore Zuck
Verifying Correctness of Transactional Memories
14:30-15:00 Naghmeh Ghafari,
Arie Gurfinkel,
Nils Klarlund, and
Richard Trefler
Algorithmic Analysis of Piecewise FIFO Systems
15:00-15:30 Xiaofang Chen,
Steven German, and
Ganesh Gopalakrishnan
Transaction Based Modeling and Verification of Hardware Protocol Implementations
15:30-15:45 Yogesh Mahajan and
Sharad Malik
Automating Hazard Checking in Transaction-Level Microarchitecture Models
15:45-16:15 Break
Session 3: Abstraction-Based Methods, Chair: Malay Ganai (NEC)
16:15-16:45 Roberto Cavada,
Alessandro Cimatti,
Anders Franzen,
Kalyanasundaram Krishnamani,
Marco Roveri, and
R. K. Shyamasundar
Computing Abstractions by integrating BDDs and SMT
16:45-17:15 Chao Wang,
Aarti Gupta, and
Franjo Ivancic
Induction in CEGAR for Detecting Counterexamples
17:15-17:30 Daniel Kroening and
Georg Weissenbacher
Lifting Propositional Interpolants to the Word-Level
Tuesday, November 13
Conference, Day 3
8:15-9:00 Breakfast
Session 1: Software Analysis Methods, Chair: Kathi Fisler (WPI)
9:00-9:30 Fadi Zaraket,
John Pape,
Margarida Jacome,
Adnan Aziz, and
Sarfraz Khurshid
COSE: a Technique for Co-optimizing Embedded Systems
9:30-10:00 Hana Chockler,
Benny Godlin,
Eitan Farchi, and
Sergey Novikov
Cross-Entropy Based Testing
10:00-10:30 Break
Session 2: Panel Discussion, Moderator: William Joyner (SRC)
10:30-12:30 Robert Jones,
Andreas Kuehlmann,
Carl Pixley
FMCAD2027: Will the 'FM' Have a Real Impact on the 'CAD'?
[slides: Joyner, Kuehlmann, Pixley]
12:30-14:00 Lunch
Location: Arbor Room (Renaissance Austin Hotel)
Session 3: Symbolic Trajectory Evaluation, Chair: Koen Claessen (Chalmers)
14:00-14:30 Yan Chen,
Yujing He,
Fei Xie, and
Jin Yang
Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation
14:30-15:00 Edward SmithA Logic for GSTE
15:00-15:30Sara Adams,
Magnus Bjork,
Tom Melham, and
Carl-Johan Seger
Automatic Abstraction in Symbolic Trajectory Evaluation
15:30-16:00 Break
Session 4: Specification Theory, Chair: Tom Melham (Oxford University)
16:00-16:30 Koen Claessen A Coverage Analysis for Safety Property Lists
16:30-17:00 Orna Kupferman and
Yoad Lustig
What triggers a behavior?
17:00-17:15 Kathi Fisler Two-Dimensional Regular Expressions for Compositional Bus Protocols
17:15-17:30 Martin Oberkönig,
Martin Schickel, and
Hans Eveking
A Quantitative Completeness Analysis for Property-Sets
17:30-18:30 All Business Meeting
19:00 Conference Banquet
Location: Ventana at Texas Culinary Academy

11400 Burnet Road Suite 2100, Austin, TX 78758
Wednesday, November 14
Conference, Day 4
8:15-9:00 Breakfast
Invited Talk, Chair: Jeremy Levitt (Mentor)
9:00-10:00 Wolfgang Kunz Formal Verification of Systems-on-Chip - Industrial Experiences and Scientific Perspectives
10:00-10:30 Break
Session 1: Industrial-Strength Verification, Chair: Rajeev Ranjan (Jasper)
10:30-11:00 Michael Case,
Alan Mishchenko, and
Robert Brayton
Automated Extraction of Inductive Invariants to Aid Model Checking
11:00-11:30 Aaron Bradley and
Zohar Manna
Checking Safety by Inductive Generalization of Counterexamples to Induction
11:30-12:00 Aaron Hurst,
Alan Mishchenko, and
Robert Brayton
Fast Minimum Register Retiming Via Binary Maximum-Flow
12:00-12:15 Adrian Seigler,
Gary Van Huben, and
Hari Mony
Formal Verification of Partial Good Self-Test Fencing Structures
12:15-12:30 Alon Flaisher,
Alon Gluska, and
Eli Singerman
Case study: Integrating FV and DV within the Verification of Intel(r) Core(TM)2 Microprocessor
12:30-14:00 Lunch
Location: Arbor Room (Renaissance Austin Hotel)
Session 2: Reasoning about Physical Systems, Chair: Daniel Kroenig (ETH Zurich)
14:00-14:30 Chao Yan and
Mark Greenstreet
Circuit-Level Verification of a High-Speed Toggle
14:30-15:00 Mohamed Zaki,
Ghiath Al Sammane,
Sofiene Tahar, and
Guy Bois
Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs
15:00-15:15 Neha Rungta,
Hyrum Carroll,
Eric Mercer,
Randall Roper,
Mark Clement, and
Quinn Snell
Analyzing Gene Relationships for Down Syndrome with Labeled Transitions Graphs
15:15-15:45 Break
Session 3: Advanced Theorem-Proving Applications, Chair: Warren Hunt (University of Texas)
15:45-16:15 Julien Schmaltz A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware
16:15-16:45 Lee Pike Modeling Time-Triggered Protocols and Verifying their Real-Time Schedules
16:45-17:00 Sandip Ray and
Jayanta Bhadra
A Mechanized Refinement Framework for Analysis of Custom Memories