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 Oberkönig, 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
_______________________________________________
Om-announce mailing list
[email protected]
http://openmath.org/mailman/listinfo/om-announce
