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

                     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:



  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