HWMCC'15 call for model checkers

[Armin Biere]

HWMCC'15

http://fmv.jku.at/hwmcc15

Affiliated to FMCAD'15

Austin, Texas, September 27 - 30, 2015

This is the 8th 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 tracks are run in the same way as in the previous three years,
except that we have to fall back to our compute cluster in Linz running
Ubuntu 14.04.3 64 bit with Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz
CPUs. This is the same hardware as used in competitions before 2014. It
is less powerful than the Aalto cluster used in 2014.

Thus the cluster we are going to use will have 8 GB main memory per
node. Solvers will have full access to one node with four cores per
node. This implies that a memory limit of 7GB will be enforced. The
main change this year is to use a substantially larger time limit of
1 hour wall clock-time. We might increase it further to even 3 hours,
depending on the number of submissions.

In order to maximize the time limit, the number of submissions will be
restricted to at most two model checkers per submitter.

As in 2014 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 increased time limit, 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, 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>.

First versions of model checkers are due on September 6.

Updates of model checkers are possible until September 13.

New benchmarks are accepted until September 13 as well.

All submission dates are anywhere on earth.


Organization

HWMCC'14 is organized by

Armin Biere, JKU Austria, and Keijo Heljanko, Aalto University Finland.


Previous Editions

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