[FOM] FMCAD 2007 Second Call for Papers [Apologies for duplicate postings]

Wed Apr 18 15:39:31 EDT 2007

                            FMCAD 2007
  International Conference on Formal Methods in Computer-Aided Design
                        http://fmcad.org/2007
                          CALL FOR PAPERS

                 November 11-14, 2007, Austin, Texas

IMPORTANT DATES (firm)
==========================================================================
Abstract Submission Deadline: April 30, 2007
Paper Submission Deadline:    May 7, 2007
Acceptance Notification:      June 21, 2007
Final Version Due:            July 28, 2007

SCOPE OF CONFERENCE
==========================================================================
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. Topics of interest for the 
technical program include, but are not limited to:

* Foundations: advancing industrial-strength technologies in model 
checking, theorem proving, equivalence checking, abstraction and 
refinement techniques, property-preserving reduction techniques, 
compositional methods, decision procedures, SAT- and BDD-based 
methods, combining deductive methods with decision procedures, and 
probabilistic methods.

* Verification applications: tools, industrial experience reports, 
and case studies. We encourage the submission of materials relating 
to novel and challenging industrial-scale applications of formal 
methods, including problem domains where formal methods worked well 
or even fell short. We also encourage submissions relating to the 
development and execution of methodologies for formal and informal 
verification strategies.

* Applications of formal methods in design: topics relating to the 
application and applicability of assertion-based verification, 
equivalence checking, transaction-level verification, semi-formal 
verification, runtime verification, simulation and testcase 
generation, coverage analysis, microcode verification, embedded 
systems, software verification, concurrent systems, timing 
verification, and formal approaches to performance and power.

* Model-based approaches: modeling and specification languages, 
system-level design and verification, design derivation and 
transformation, and correct-by-construction methods.

* Formal methods for the design and verification of emerging and 
novel technologies: nano, quantum, biological, video, gaming, and 
multimedia applications.

PAPER SUBMISSIONS
==========================================================================
Submissions must be made electronically in PDF format through the 
FMCAD Website, http://fmcad.org/2007. The proceedings will be 
published by the IEEE and will be available online in the ACM Digital 
Library and the IEEE Xplore Digital Library. There are two categories 
of papers:

A. REGULAR PAPERS

Regular papers are limited to 8 pages using the IEEE Transactions 
format on letter-size
paper with a 10-point font size (see 
http://www.ieee.org/portal/pages/pubs/transactions/stylesheets.html). 
We recommend that self-citations be written in the third person, 
though authors will be required to identify themselves on their 
submissions. Submissions must contain original research that has not 
been previously published, nor concurrently submitted for 
publication. Any partial overlap with any published or concurrently 
submitted paper must be clearly indicated. If experimental results 
are reported, authors are strongly encouraged to provide adequate 
access to their data so that results can be independently verified. 
Papers should contain a short abstract of approximately 150 words 
clearly stating the contribution of the submission. Refer to 
http://fmcad.org/2007 for evolving submission details. A small number 
of accepted papers will be considered for a Distinguished Paper Award.

B. SHORT PAPERS

The page limit is 4 pages using the same format as for regular 
papers. Short papers can describe applications, case studies, 
industrial experience reports, emerging results, or implemented tools 
with novel features. A demonstration will be required for accepted tool papers.

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
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

PANELS
==========================================================================
Chair:                William Joyner, Semiconductor Research Corporation, USA
Participants:         Robert Jones, Intel Corp., USA
                       Andreas Kuehlmann, Cadence Laboratories, USA
                       Carl Pixley, Synopsys, USA

This panel will focus broadly upon "CAD in the 22nd Century!" It will 
address what design, verification, synthesis, etc. will be like given 
a long enough time-line that most of today's barriers and 
impossibilities have been addressed through technological advances. 
This panel should spark a lively discussion, and help identify a 
variety of open research problems that require attention along this 
CAD evolution.

TUTORIALS
==========================================================================
Robert Brayton, University of California at Berkeley, USA
This tutorial will focus upon the synergy between logic synthesis and 
verification, and numerous advances in the state-of-the-art thereof.

Randal Bryant, Carnegie-Mellon University, USA
This tutorial will address the use of word-level abstractions to 
stretch the capacity barrier of automated verification tools, while 
retaining bit-level accuracy in verification results.

Niklas Een, Cadence, USA
This tutorial illuminates the numerous engineering decisions, many 
undocumented in the literature, that one faces when using and tuning 
a state-of-the-art SAT solver in an industrial setting.

Farid Najm, University of Toronto, Canada
This tutorial will demonstrate the increasing need for low-power 
design solutions, covering the link from high-level design to power 
dissipation of the final silicon chip, power modeling and estimation 
techniques, and numerous techniques for power optimizations.

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