[FOM] FMCAD 2007 Call for Participation

by way of Martin Davis <martin@eipye.com> jasonb at austin.ibm.com
Fri Aug 31 17:26:04 EDT 2007

                           FMCAD 2007
  International Conference on Formal Methods in Computer-Aided Design
                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.


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

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

More information about the FOM mailing list