11-14 November 2007
Austin TX, U.S.A.
FMCAD 2007
International Conference on Formal Methods in Computer-Aided Design
http://fmcad.org/2007
November 11-14, 2007, Austin, Texas
CALL FOR PARTICIPATION
---------------------------------------------------------------
Early Registration will open mid-September
Refer to http://fmcad.org/2007 for more information and updates
---------------------------------------------------------------
FMCAD 2007 is the seventh in a series of
conferences on the theory and application of
formal methods in hardware and system design and
verification. In 2005, the bi-annual FMCAD and
sister conference CHARME decided to merge to form
an annual conference with a unified community.
The resulting unified FMCAD provides a leading
international forum to researchers and
practitioners in academia and industry for
presenting and discussing groundbreaking methods,
technologies, theoretical results, and tools for
formally reasoning about computing systems, as
well as open challenges therein. FMCAD2007 will
include a full day of tutorials (see below), and
will be co-located with the ACL2 Workshop.
Program
============================================================================
====
Sunday, November 11
8:30-9:00 Welcome and Opening Remarks
9:00-10:00 Robert Brayton
The Synergy between Logic Synthesis and Equivalence
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
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
17:30-19:00 Panel Presentation + Discussion
The Business of Formal Verification
Moderator: Aarti Gupta
19:00 Reception
Monday, November 12
8:30-9:00 Welcome and Opening Remarks
Invited Talk
9:00-10:00 Eli Singerman
Verification of Embedded Software in Industrial
Microprocessors
10:00-10:30 Break
Session 1: SAT-Based Methods
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
Session 2: High-Level System Analysis
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
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
Session 1: Software Analysis Methods
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 Presentations + Discussion
10:30-12:30 FMCAD 2027: Will the 'FM' Have a Real Impact on the 'CAD'?
Moderator: William Joyner (SRC)
Panelists: Robert Jones, Andreas Kuehlmann, Carl Pixley
12:30-14:00 Lunch
Session 3: Symbolic Trajectory Evaluation
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 Smith
A Logic for GSTE
15:00-15:30 Sara Adams, Magnus Bjork, Tom Melham, and Carl-Johan Seger
Automatic Abstraction in Symbolic Trajectory Evaluation
15:30-16:00 Break
Session 4: Specification Theory
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 Oberknig, Martin Schickel, and Hans Eveking
A Quantitative Completeness Analysis for Property-Sets
17:30-18:30 Business Meeting
19:00 Conference Banquet
Location: Ventana at Texas Culinary Academy
Wednesday, November 14
Invited Talk
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
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
Session 2: Reasoning about Physical Systems
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
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
Organization
============================================================================
====
Chairs: Jason Baumgartner, IBM Corporation, USA
Mary Sheeran, Chalmers University of Technology,
Sweden
Benchmarks: Panagiotis Manolios, Georgia Institute of
Technology, USA
Local Arrangements: Andy Martin, IBM Corporation, USA
Panels: Aarti Gupta, NEC Laboratories America, USA
William Joyner, Semiconductor Research Corporation,
USA
Publicity: Alper Sen, Freescale Semiconductor Inc., USA
Tutorials: Natasha Sharygina, University of Lugano, Switzerland
Webmasters: Hari Mony, IBM Corporation, USA
Sandip Ray, University of Texas, USA
Program Committee
============================================================================
====
Mark Aagaard, University of Waterloo, Canada
Jason Baumgartner, IBM Corporation, USA
Armin Biere, Johannes Kepler University, Austria
Per Bjesse, Synopsys, USA
Dominique Borrione, Grenoble University, France
Gianpiero Cabodi, Politecnico di Torino, Italy
Alessandro Cimatti, ITC-irst, Trento, Italy
Koen Claessen, Chalmers University of Technology, Sweden
Cindy Eisner, IBM Haifa Research Laboratory, Israel
Steven German, IBM Research Division, USA
Ganesh Gopalakrishnan, University of Utah, USA
Aarti Gupta, NEC Laboratories America, USA
Alan J. Hu, University of British Columbia, Canada
Warren Hunt, University of Texas, USA
Steven Johnson, Indiana University, USA
Robert Jones, Intel Corp., USA
Daniel Kroening, ETH Zurich, Switzerland
Andreas Kuehlmann, Cadence Laboratories, USA
Wolfgang Kunz, University of Kaiserslautern, Germany
Jeremy Levitt, Mentor Graphics, USA
Panagiotis Manolios, Georgia Institute of Technology, USA
Andy Martin, IBM Research Division, USA
Tom Melham, Oxford University, UK
Alan Mishchenko, University of California at Berkeley, USA
Ken McMillan, Cadence Labs, USA
John O'Leary, Intel Corp., USA
Wolfgang Paul, Saarland University, Germany
Carl Pixley, Synopsys, USA
Natasha Sharygina, University of Lugano, Switzerland
Mary Sheeran, Chalmers University of Technology, Sweden
Anna Slobodova, Intel Corp., USA
Richard Trefler, University of Waterloo, Canada