[ Results |  Setup |  Submission |  Organization |  Previous Editions ]

HWMCC'15

Affiliated to FMCAD'15

Austin, Texas, September 27 - 30, 2015

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

Results

Presentation Biere-HWMCC15-talk.pdf

SINGLE instances hwmcc15-benchmarks-single.7z
SINGLE zummaries hwmcc15-zummaries-single.7z
SINGLE log files scripts and plots hwmcc15-logs-single.7z
SINGLE merged results hwmcc15-single.csv

LIVE instances hwmcc15-benchmarks-live.7z
LIVE zummaries hwmcc15-zummaries-live.7z
LIVE log files scripts and plots hwmcc15-logs-live.7z
LIVE merged results hwmcc15-live.csv

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 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" <biere@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'15 is organized by

Armin Biere, Johannes Keplers University, Linz, Austria
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