==============================================================
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
https://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 https://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
https://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 <biere@jku.at> 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