============================================================== We apologize if you receive multiple copies of this CFP. Please distribute to anyone who may be interested. ============================================================== Call for Papers ********************************************************* First Hardware Verification Workshop 2010 http://fmv.jku.at/hwvw10 July 15, 2010 Edinburgh, United Kingdom affiliated with CAV'10 at FLOC'10 ********************************************************* HWVW'10 is the first workshop devoted to formal verification of hardware design. Formal verification methods, and model checking in particular, are extensively used in the industry where they are relied upon to ensure quality and robustness. However, design size and complexity are growing faster than verification capacity. This phenomenon, known as the "verification gap", is one of the biggest concerns in the industry; yet recently we have seen a steady dwindling in the number of publications that specifically target hardware. The purpose of this workshop is to rekindle the interest in and enthusiasm for hardware verification. We aim to encourage new and daring directions, provide a stage for ideas in early developmental stages, and initiate discussions defining the challenges that remain to be tackled. The scope of the workshop will include both general research in formal verification techniques for hardware as well as specific issues related to the development of model checking tools. The workshop will include the Hardware Model Checking Competition, which is the third event in this series. Researchers from both academia and industry are invited to submit solvers and benchmark examples. We also welcome tool descriptions that describe unique features and implementation details of model checkers submitted to the competition. ---------------------------------------------------------------- Topics of interest to the workshop include, but are not limited to: - model checking technology and system descriptions - improvements in reasoning engines related to verification - formal approaches to synthesis, modelling, and verification - formal verification technology in synthesis - applications and case studies in verification Focus is on hardware but closely related work on embedded software or SW/HW codesign is also welcome. ---------------------------------------------------------------- Invited speakers: Cindy Eisner, IBM Haifa Research Lab, Israel Sharad Malik, Princeton University, USA ---------------------------------------------------------------- Authors of original papers accepted to HWVW'10 will be invited to submit an extended journal version of their work to a special issue of Formal Methods in System Design (FMSD). ---------------------------------------------------------------- Paper submission: Papers should be written in LaTeX using the LNCS format without modifications to the default configuration. Three types of paper submissions are solicited: (1) Original papers, containing research not published elsewhere. These will be considered for the special issue in FMSD. (page limit: 12 pages) (2) Early stage papers, containing new and exciting ideas that have not yet developed into validated results. (page limit: 8 pages) (3) Presentation only talks, describing recently published work that is of interest to this community. (one page abstract + original paper) Paper submission is handled through EasyChair: http://www.easychair.org/conferences/?conf=hwvw10 ---------------------------------------------------------------- Important dates for paper submission: Submission deadline: March 26, 2010 Author notification: April 23, 2010 Workshop: July 15, 2010 ---------------------------------------------------------------- For the model checking competition we solicit: Hardware model checking benchmarks, preferably in the AIGER format (see http://fmv.jku.at/aiger). At this point we will use one single safety property per benchmark. Models with multiple safety properties will be split into multiple benchmarks. Please contact the competition chairs if you want to submit benchmarks in other formats or benchmarks with different characteristics. Model checkers should be able to read the AIGER format and also produce witnesses according to the AIGER standard. See again the AIGER format description available at http://fmv.jku.at/aiger. If your model checker can not read AIGER or can not produce proper AIGER witness please contact the competition chairs. The computing platform consists of 64-bit x86 Linux machines, which of course also can run 32-bit binaries. There will be a memory limit of 7 GB and a time limit of 900 seconds. We would prefer to have benchmarks that can be published at least for academic research, but for model checkers we do not require to release source code nor to publish a binary. The submission can be a binary executable only and will be kept confidential. Benchmarks and model checker submission is handled via Email. Please contact Armin Biere for more details. ---------------------------------------------------------------- Important dates for benchmark and model checker submission: Benchmark submission: May 28, 2010 Model checker submission: June 4, 2010 Competition results: July 15, 2010 ---------------------------------------------------------------- HWVW'10 Chairs: Armin Biere, Johannes Kepler University, Austria Karen Yorav, IBM, Israel MC competition chairs: Armin Biere, Johannes Kepler University, Austria Koen Claessen, Chalmers University of Technology, Sweden Program Committee: Armin Biere, Johannes Kepler University, Austria Roderick Bloem, Graz University of Technology, Austria Alessandro Cimatti, FBK-IRST, Italy Koen Claessen, Chalmers University of Technology, Sweden Zurab Khasidashvili, Intel, Israel Daniel Kroening, University of Oxford, United Kingdom Sanjit Seshia, University of California, Berkeley, USA Karen Yorav, IBM, Israel