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