HWMCC'17 Call for Model Checkers and Benchmarks
Armin Biere
HWMCC'17
Affiliated to FMCAD'17
Vienna, Austria, October 2 - 6, 2017
This is the 9th competitive event for hardware model checkers.
Setup
The competition consists of a single safety property track (SINGLE), a (single) liveness property track (LIVE), and a deep bound track (DEEP), but no multiple property track. The winner of the deep bound track will receive an award of $500 sponsored by Oski Technology.
The tracks are run in the same way as in the previous four incarnations of the competition, except that we are going to use our new cluster running Ubuntu 16.04.2 64 bit. Each cluster node has two Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz CPUs and 128 GB of main memory.
Each solver will have full access to both processors on one node, thus combined 16 cores (32 virtual cores) and 128 GB of main memory. Accordingly a memory limit of 120GB will be enforced. As in the last competition in 2015 we will further use a time limit of 1 hour of wall clock-time.
Also as before the number of submissions will be restricted to at most two model checkers per submitter and model checkers are required to produce witnesses in the SINGLE track. These witnesses will be checked by the AIGSIM tool, which is part of the AIGER tools.
Except for the new hardware, competition rules, as well as input and output formats did not change. Please consult the pages of previous competitions (see for instance HWMCC'12 or below) for more details.
Again as in 2014 and 2015, in order to avoid glitches in interpreting the format, the SINGLE track will only use AIGER pre 1.9 single property benchmarks, with the single bad state property encoded as an output (MILOA header with O = 1). All latches are implicitly initialized to zero as it is the default in the pre 1.9 AIGER format.
There is no change in the LIVE track nor in the DEEP track. Solvers intended to participate in the DEEP track are run in the SINGLE track and are expected to print reached bounds as in previous years (see for instance HWMCC'12).
Submission
Email submission to "Armin Biere" <bi...@jku.at>.
Registration and first versions of model checkers are due on September 7.
Updates of model checkers are possible until September 14.
New benchmarks are accepted until September 13 as well.
All submission dates are anywhere on earth.
Organization
HWMCC'17 is organized by
Armin Biere, Johannes Keplers University, Linz, Austria
Tom van Dijk, Johannes Keplers University, Linz, Austria
Keijo Heljanko, Aalto University, Finland
Previous Editions
HWMCC'15 at FMCAD'15,
Austin, USA
HWMCC'14 at CAV'14, FLoC'14 Olympic Games, Vienna,
Austria
HWMCC'13 at FMCAD'13,
Portland, USA
HWMCC'12 at FMCAD'12,
Cambridge, UK
HWMCC'11 at FMCAD'11,
Austin, USA
HWMCC'10 at CAV'10, FloC'10,
Edinburgh, UK
HWMCC'08 at CAV'08, Princeton, USA
HWMCC'07 at CAV'07, Berlin, Germany