FMCAD 2009
First Call for Papers
International Conference on Formal Methods in Computer-Aided Design

University of Texas at Austin, Texas, USA
November 15 - 18, 2009

http://fmv.jku.at/fmcad09

Important Dates

Abstract Submission: May 15

Paper Submission: May 22

Author Notification: July 31

Final Version: August 21

Conference: November 15-18

Conference Scope

FMCAD 2009 is the ninth 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 its 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 novel methods, technologies,
theoretical results, and tools for formally reasoning about
computing systems, as well as open challenges therein.

Topics of Interest

Foundations

Advancing Industrial-Strength Technologies in Model Checking,
Theorem Proving, Equivalence Checking, Abstraction and Refinement
Techniques, Property-Preserving Reduction Techniques,
Compositional Methods, Decision Procedures, SMT Solvers,
SAT- and BDD-Based Methods, Probabilistic Methods,
Combining Deductive Methods with Decision Procedures.

Verification Applications

Tools, Industrial Experience Reports, 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,
Formal Approaches to Performance and Power.

Model-Based Approaches

Modeling and Specification Languages,
System-Level Design and Verification,
Design Derivation and Transformation,
Correct-by-Construction Methods.

Novel Technologies

Formal methods for the design and verification of emerging and novel
technologies, such as

Nano, Quantum, Biological, Video Gaming, and Multimedia Applications.

Paper Submissions

Submissions must be made electronically in PDF format
via EasyChair. More details will be provided at
http://fmv.jku.at/fmcad09/submissions.html.

The proceedings are planned to be published by IEEE and ACM and will
then be available online in the ACM Digital Library and the IEEE
Xplore Digital Library. Two categories of papers can be submitted:
regular papers (8 pages), containing original research that has not
been previously published, nor concurrently submitted for publication;
and short papers (4 pages), describing applications, case studies,
industrial experience reports, emerging results, or implemented tools
with novel features.

Regular and short papers must use 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.

A small number of accepted papers will be considered for a distinguished
paper award.

General Chairs

Armin Biere, Johannes Kepler University, Linz, Austria
Carl Pixley, Synopsys Inc., Hillsboro, USA

Local Arrangement

Sandip Ray, University of Texas at Austin, USA
Anna Slobodova, Centaur Technology, USA

Steering Commitee

Jason Baumgartner, IBM, USA
Aarti Gupta, NEC Labs America, USA
Warren Hunt, University of Texas at Austin, USA
Panagiotis Manolios, Northeastern University, USA
Mary Sheeran, Chalmers University of Technology, Sweden

Program Committee

Jason Baumgartner, IBM, USA
Armin Biere, Johannes Kepler University, Austria
Per Bjesse, Synopsys, USA
Roderick Bloem, Graz University of Technology, Austria
Gianpiero Cabodi, Politecnico di Torino, Italy
Supratik Chakraborty, IIT Bombay, India
Alessandro Cimatti, FBK-IRST, Italy
Koen Claessen, Chalmers University of Technology, Sweden
Leonardo de Moura, Microsoft, USA
Wolfgang Ecker, Infineon, Germany
Masahiro Fujita, University of Tokyo, Japan
Ganesh Gopalakrishnan, University of Utah, USA
Aarti Gupta, NEC Labs America, USA
Ziyad Hanna, Jasper, USA
John Harrison, Intel, USA
Alan Hu, University of British Columbia, Canada
Warren Hunt, University of Texas at Austin, USA
Daniel Kroening, University of Oxford, UK
Thomas Kropf, Robert Bosch GmbH, Germany
Andreas Kuehlmann, Cadence, USA
Wolfgang Kunz, University of Kaiserslautern, Germany
Panagiotis Manolios, Northeastern University, USA
Joao Marques-Silva, University College Dublin, Ireland
Anmol Mathur, Calypto, USA
Ken McMillan, Cadence, USA
Tom Melham, University of Oxford, UK
Ganapathy Parthasarathy, Real Intent, USA
Lee Pike, Galois, USA
Carl Pixley, Synopsys, Hillsboro, USA
Mukul Prasad, Fujitsu, USA
Sandip Ray, University of Texas at Austin, USA
Anna Slobodova, Centaur Technology, USA
Ofer Strichman, Technion, Israel
Helmut Veith, Technical University of Darmstadt, Germany
Karen Yorav, IBM, Israel