[Om-announce] FMCAD 2007 Call for Participation

[jasonb at austin.ibm.com]

                          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