<tt><font size=3>FMCAD 2014 - FORMAL METHODS IN COMPUTER-AIDED DESIGN</font></tt>
<br>
<br><tt><font size=3>FIRST CALL FOR PAPERS</font></tt>
<br>
<br><tt><font size=3>International Conference on </font></tt>
<br><tt><font size=3>Formal Methods in Computer-Aided Design (FMCAD)</font></tt>
<br>
<br><tt><font size=3>Lausanne, Switzerland, October 21-24, 2014</font></tt>
<br><a href=http://www.fmcad.org/FMCAD14><tt><font size=3 color=blue>http://www.fmcad.org/FMCAD14</font></tt></a>
<br>
<br><tt><font size=3>The conference includes the FMCAD student forum;</font></tt>
<br><tt><font size=3>it is collocated with MEMOCODE, DIFTS, and the</font></tt>
<br><tt><font size=3>Hardware Model Checking Competition 2014 FMCAD Edition.</font></tt>
<br>
<br><tt><font size=3>IMPORTANT FMCAD DATES</font></tt>
<br>
<br><tt><font size=3>Abstract Submission: Tuesday, May 6</font></tt>
<br><tt><font size=3>Paper Submission: Friday, May 16</font></tt>
<br><tt><font size=3>Author Response Period: June 23-27</font></tt>
<br><tt><font size=3>Author Notification: July 25</font></tt>
<br><tt><font size=3>Camera-Ready Version: August 15</font></tt>
<br><tt><font size=3>Conference: October 21-24</font></tt>
<br>
<br><tt><font size=3>CONFERENCE SCOPE </font></tt>
<br>
<br><tt><font size=3>FMCAD 2014 is the 14th in a series of conferences
on the</font></tt>
<br><tt><font size=3>theory and application of formal methods in computer-aided</font></tt>
<br><tt><font size=3>design and verification of computer systems and related</font></tt>
<br><tt><font size=3>topics. FMCAD provides a leading international forum
to</font></tt>
<br><tt><font size=3>researchers and practitioners in academia and industry
for</font></tt>
<br><tt><font size=3>presenting and discussing novel methods, technologies,</font></tt>
<br><tt><font size=3>theoretical results, tools, and open challenges in
formal</font></tt>
<br><tt><font size=3>reasoning.</font></tt>
<br>
<br><tt><font size=3>FMCAD employs a rigorous peer-review process and is
devoted</font></tt>
<br><tt><font size=3>to maximizing the dissemination of papers. Accepted
papers</font></tt>
<br><tt><font size=3>are distributed through both ACM and IEEE digital</font></tt>
<br><tt><font size=3>libraries. In addition, published articles are made</font></tt>
<br><tt><font size=3>available freely on the conference page and the authors</font></tt>
<br><tt><font size=3>retain the copyright. There are no publication fees.
At</font></tt>
<br><tt><font size=3>least one of the authors is required to register for
the</font></tt>
<br><tt><font size=3>conference and present the accepted paper.</font></tt>
<br>
<br><tt><font size=3>FMCAD 2014 will be co-located with MEMOCODE, the ACM/IEEE</font></tt>
<br><tt><font size=3>International Conference on Formal Methods and Models
for</font></tt>
<br><tt><font size=3>Codesign, in Lausanne, Switzerland. MEMOCODE
will take</font></tt>
<br><tt><font size=3>place from October 19 to 20, followed by a joint</font></tt>
<br><tt><font size=3>FMCAD/MEMOCODE tutorial day on October 21. FMCAD
will</font></tt>
<br><tt><font size=3>continue from October 22 to 24, 2014.</font></tt>
<br>
<br><tt><font size=3>TOPICS OF INTEREST</font></tt>
<br>
<br><tt><font size=3>FMCAD welcomes submission of papers reporting original</font></tt>
<br><tt><font size=3>research on advances in all aspects of formal methods</font></tt>
<br><tt><font size=3>technology and its application to computer-aided design.</font></tt>
<br><tt><font size=3>Topics of interest include, but are not limited to,
the</font></tt>
<br><tt><font size=3>following:</font></tt>
<br>
<br><tt><font size=3>-- Model checking, theorem proving, equivalence checking,</font></tt>
<br><tt><font size=3> abstraction and reduction, compositional
methods,</font></tt>
<br><tt><font size=3> decision procedures at the bit- and word-level,</font></tt>
<br><tt><font size=3> probabilistic methods, combinations of
deductive methods</font></tt>
<br><tt><font size=3> and decision procedures.</font></tt>
<br>
<br><tt><font size=3>-- Synthesis and compilation for computer system</font></tt>
<br><tt><font size=3> descriptions, modeling, specification,
and implementation</font></tt>
<br><tt><font size=3> languages, formal semantics of languages
and their</font></tt>
<br><tt><font size=3> subsets, model-based design, design derivation
and</font></tt>
<br><tt><font size=3> transformation, correct-by-construction
methods.</font></tt>
<br>
<br><tt><font size=3>-- Application of formal and semi-formal methods to</font></tt>
<br><tt><font size=3> functional and non-functional specification
and</font></tt>
<br><tt><font size=3> validation of hardware and software,
including timing and</font></tt>
<br><tt><font size=3> power modeling, verification of computing
systems on all</font></tt>
<br><tt><font size=3> levels of abstraction, system-level design
and</font></tt>
<br><tt><font size=3> verification for embedded and cyberphysical
systems,</font></tt>
<br><tt><font size=3> hardware-software co-design and verification,</font></tt>
<br><tt><font size=3> transaction-level verification.</font></tt>
<br>
<br><tt><font size=3>-- Experience with the application of formal and semi-formal</font></tt>
<br><tt><font size=3> methods to industrial-scale designs.
Tools that represent</font></tt>
<br><tt><font size=3> formal verification enablement, new features,
or a</font></tt>
<br><tt><font size=3> substantial improvement in the automation
of formal</font></tt>
<br><tt><font size=3> methods.</font></tt>
<br>
<br><tt><font size=3>-- Application of formal methods in areas beyond computer</font></tt>
<br><tt><font size=3> systems, including formal methods describing
processes</font></tt>
<br><tt><font size=3> studied in other areas of science, engineering,
and</font></tt>
<br><tt><font size=3> humanities.</font></tt>
<br>
<br><tt><font size=3>SUBMISSIONS</font></tt>
<br>
<br><tt><font size=3>Submissions must be made electronically in PDF format</font></tt>
<br><tt><font size=3>through a link available on the FMCAD web site</font></tt>
<br>
<br><a href=http://fmcad.org/FMCAD14><tt><font size=3 color=blue>http://fmcad.org/FMCAD14</font></tt></a>
<br>
<br><tt><font size=3>Two categories of papers can be submitted: regular
papers (8</font></tt>
<br><tt><font size=3>pages) and short papers (4 pages) containing ideas
and</font></tt>
<br><tt><font size=3>results that can be described succinctly. Both
regular and</font></tt>
<br><tt><font size=3>short papers must use the IEEE Transactions format
on</font></tt>
<br><tt><font size=3>letter-size paper with a 10-point font size.</font></tt>
<br>
<br><tt><font size=3>Submissions must contain original research that has
not been</font></tt>
<br><tt><font size=3>previously published, nor concurrently submitted for</font></tt>
<br><tt><font size=3>publication. Any partial overlap with published or</font></tt>
<br><tt><font size=3>concurrently submitted papers must be clearly indicated.
If</font></tt>
<br><tt><font size=3>experimental results are reported, authors are strongly</font></tt>
<br><tt><font size=3>encouraged to provide adequate access to their data
so that</font></tt>
<br><tt><font size=3>results can be independently verified.</font></tt>
<br>
<br><tt><font size=3>A small number of accepted papers will be considered
for a</font></tt>
<br><tt><font size=3>distinguished paper award. Recently awarded papers
include:</font></tt>
<br>
<br><tt><font size=3>* "An SMT Based Method for Optimizing Arithmetic</font></tt>
<br><tt><font size=3> Computations in Embedded Software Code",
Hassan Eldib and</font></tt>
<br><tt><font size=3> Chao Wang (2013)</font></tt>
<br>
<br><tt><font size=3>* "A quantifier-free SMT encoding of non-linear
hybrid</font></tt>
<br><tt><font size=3> automata", Alessandro Cimatti, Sergio
Mover and Stefano</font></tt>
<br><tt><font size=3> Tonetta (2012)</font></tt>
<br>
<br><tt><font size=3>* "An Incremental Approach to Model Checking
Progress Properties",</font></tt>
<br><tt><font size=3> Aaron Bradley, Fabio Somenzi, Zyad Hassan and
Yan Zhang (2011)</font></tt>
<br>
<br><tt><font size=3>* "Applying SMT in Symbolic Execution of Microcode",
Anders</font></tt>
<br><tt><font size=3> Franzen, Alessandro Cimatti, Alexander Nadel,
Roberto</font></tt>
<br><tt><font size=3> Sebastiani, and Jonathan Shalev (2010)</font></tt>
<br>
<br><tt><font size=3>STUDENT FORUM</font></tt>
<br>
<br><tt><font size=3>FMCAD 2014 will host a Student Forum that provides
a</font></tt>
<br><tt><font size=3>platform for graduate students at any career stage
to</font></tt>
<br><tt><font size=3>introduce their research to the wider Formal Methods</font></tt>
<br><tt><font size=3>community, and solicit feedback. Submissions for the
event</font></tt>
<br><tt><font size=3>must be short reports describing research ideas or
ongoing</font></tt>
<br><tt><font size=3>work that the student is currently pursuing, and must
be</font></tt>
<br><tt><font size=3>within the scope of FMCAD. Work, part of which
has been</font></tt>
<br><tt><font size=3>previously published, will be considered; the novel
aspect</font></tt>
<br><tt><font size=3>to be addressed in future work must be clearly described
in</font></tt>
<br><tt><font size=3>such cases.</font></tt>
<br>
<br><tt><font size=3>The event will consist of short presentations by the
student</font></tt>
<br><tt><font size=3>authors of each accepted submission, and of a poster
that</font></tt>
<br><tt><font size=3>will be on display throughout the duration of the</font></tt>
<br><tt><font size=3>conference. Accepted submissions will be listed,
with title</font></tt>
<br><tt><font size=3>and author name, in the event description in the conference</font></tt>
<br><tt><font size=3>proceedings. The authors will also have the
option to</font></tt>
<br><tt><font size=3>upload their poster and presentation to the FMCAD
webpage.</font></tt>
<br>
<br><tt><font size=3>Limited funds will be available for travel assistance
for </font></tt>
<br><tt><font size=3>students with accepted contributions.</font></tt>
<br>
<br><tt><font size=3>CO-LOCATED EVENTS</font></tt>
<br>
<br><tt><font size=3>The following meetings will be co-located with this
year's edition:</font></tt>
<br>
<br><tt><font size=3>-- MEMOCODE 2014, the ACM/IEEE International Conference
on</font></tt>
<br><tt><font size=3> Formal Methods and Models for Codesign</font></tt>
<br><tt><font size=3> ( </font></tt><a href="http://www.memocode-conference.com/"><tt><font size=3 color=blue>http://www.memocode-conference.com</font></tt></a><tt><font size=3>
)</font></tt>
<br>
<br><tt><font size=3>-- DIFTS 2014, International Workshop on Design and</font></tt>
<br><tt><font size=3> Implementation of Formal Tools and Systems</font></tt>
<br><tt><font size=3> ( </font></tt><a href=http://fmgroup.polito.it/cabodi/difts2014/><tt><font size=3 color=blue>http://fmgroup.polito.it/cabodi/difts2014/</font></tt></a><tt><font size=3>
)</font></tt>
<br>
<br><tt><font size=3>-- We are also proud to host this year's </font></tt>
<br><tt><font size=3> Hardware Model Checking Competition 2014
FMCAD Edition</font></tt>
<br>
<br><tt><font size=3>ORGANIZING COMMITTEE</font></tt>
<br>
<br><tt><font size=3>PROGRAM CHAIRS</font></tt>
<br><tt><font size=3>Koen Claessen, Chalmers University of Technology</font></tt>
<br><tt><font size=3>Viktor Kuncak, EPFL</font></tt>
<br>
<br><tt><font size=3>LOCAL ARRANGEMENT CHAIR</font></tt>
<br><tt><font size=3>Viktor Kuncak, EPFL</font></tt>
<br>
<br><tt><font size=3>PUBLICATION CHAIR</font></tt>
<br><tt><font size=3>Barbara Jobstmann, EPFL, Jasper DA, and CNRS/Verimag</font></tt>
<br>
<br><tt><font size=3>STUDENT FORUM CHAIR</font></tt>
<br><tt><font size=3>Ruzica Piskac, Yale University </font></tt>
<br>
<br><tt><font size=3>PUBLICITY CHAIR</font></tt>
<br><tt><font size=3>Mitra Purandare, IBM Research Lab, Zurich </font></tt>
<br>
<br><tt><font size=3>PROGRAM COMMITTEE</font></tt>
<br>
<br><tt><font size=3>Jason Baumgartner, IBM</font></tt>
<br><tt><font size=3>Dirk Beyer, University of Passau</font></tt>
<br><tt><font size=3>Armin Biere, Johannes Kepler University</font></tt>
<br><tt><font size=3>Per Bjesse, Synopsys</font></tt>
<br><tt><font size=3>Nikolaj Bjorner, Microsoft Research</font></tt>
<br><tt><font size=3>Roberto Bruttomesso, Atrenta</font></tt>
<br><tt><font size=3>Gianpiero Cabodi, Politecnico di Torino</font></tt>
<br><tt><font size=3>Hana Chockler, King's College</font></tt>
<br><tt><font size=3>Alessandro Cimatti, FBK-irst</font></tt>
<br><tt><font size=3>Koen Claessen (Chair), Chalmers University of Technology</font></tt>
<br><tt><font size=3>Bruno Dutertre, SRI International</font></tt>
<br><tt><font size=3>Ziyad Hanna, Jasper Design Automation</font></tt>
<br><tt><font size=3>Keijo Heljanko, Aalto University</font></tt>
<br><tt><font size=3>Alan Hu, University of British Columbia</font></tt>
<br><tt><font size=3>Warren Hunt, University of Texas</font></tt>
<br><tt><font size=3>Susmit Jha, Strategic CAD Lab, Intel</font></tt>
<br><tt><font size=3>Daniel Kroening, University of Oxford</font></tt>
<br><tt><font size=3>Viktor Kuncak (Chair), EPFL</font></tt>
<br><tt><font size=3>Panagiotis Manolios, Northeastern University</font></tt>
<br><tt><font size=3>Ken McMillan, Microsoft Research</font></tt>
<br><tt><font size=3>Katell Morin-Allory, TIMA Laboratory, Grenoble</font></tt>
<br><tt><font size=3>Lee Pike, Galois, Inc.</font></tt>
<br><tt><font size=3>Ruzica Piskac, Yale University</font></tt>
<br><tt><font size=3>Mitra Purandare, IBM Research Lab, Zurich</font></tt>
<br><tt><font size=3>Sandip Ray, Intel Corporation</font></tt>
<br><tt><font size=3>Philipp Ruemmer, Uppsala University</font></tt>
<br><tt><font size=3>Andrey Rybalchenko, Microsoft Research Cambridge</font></tt>
<br><tt><font size=3>Julien Schmaltz, TU Eindhoven</font></tt>
<br><tt><font size=3>Natasha Sharygina, Universita' della Svizzera Italiana</font></tt>
<br><tt><font size=3>Anna Slobodova, Centaur Technology</font></tt>
<br><tt><font size=3>Niklas Sorensson, Chalmers University of Technology</font></tt>
<br><tt><font size=3>Daryl Stewart, ARM</font></tt>
<br><tt><font size=3>Cesare Tinelli, The University of Iowa</font></tt>
<br><tt><font size=3>Martin Vechev, ETH Zurich</font></tt>
<br><tt><font size=3>Thomas Wahl, Northeastern University</font></tt>
<br><tt><font size=3>Georg Weissenbacher, Vienna University of Technology
</font></tt>
<br>
<br><tt><font size=3>STEERING COMMITTEE</font></tt>
<br>
<br><tt><font size=3>Jason Baumgartner, IBM, USA</font></tt>
<br><tt><font size=3>Armin Biere, Johannes Kepler University in Linz, Austria</font></tt>
<br><tt><font size=3>Alan Hu, University of British Columbia, Canada </font></tt>
<br><tt><font size=3>Warren Hunt, University of Texas at Austin, USA</font></tt>