Affiliated to FMCAD'17

Vienna, Austria, October 2 - 6, 2017

This is the 9th competitive event for hardware model checkers.


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).


Email submission to "Armin Biere" <biere@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.


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

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