[ results | format | setup | submission | organization | history ]

HWMCC'20

Affiliated to FMCAD'20

September 21 - 24, 2020

This was the 11th competitive event for hardware model checkers.

Results

Congratulations go to the overall winner AVR: Abstractly Verifying Reachability by Aman Goel and Karem Sakallah (Univ. of Michigan).

The slides summarizing the results and presented in the HWMCC session at FMCAD are available as hwmcc20slides.pdf.
In total we awarded 27 "medals", with 3 medals in each of the BV, BV+Arrays and the combined category, with SAT, UNSAT, and SAT+UNSAT (all) sub-tracks.

The selected (single property) benchmarks are available as hwmcc20benchmarks.tar.xz both in BTOR as well as bit-blasted in AIGER format.

The log files of the runs are available as hwmcc20runs.tar.xz.

We also provide supplementary tables with additional model checkers:

Finally, here are CSV files with one row per benchmark and one column per model checker:

Note that the bounds columns are only computed for AIGER model checkers and actually off by one in many cases (220 out of 324 BV benchmarks). We had to remove constraints with the tool `aigunconstraint' due to discrepancies showing up with constraints. However, not all bit-blasted AIGER models had constraints (actually 104 did not). You find those by grepping for `aigunconstraint' in the provided error files `.err' files.

The plots and tables and are generated by the HWMCC'20 version of zummarize available as hwmcc20zummarize.tar.xz.

Format

In 2020 we only had a word-level track based on the BTOR2 format, which is described in our CAV'18 paper. The Btor2Tools tool suite provides a generic parser Btor2Parser and a simulator BtorSIM, which are useful for parsing and random simulation of BTOR2 models, as well as for witness checking. There is also a simple bounded model checker BtorMC, distributed as part of Boolector.

Due to the low number of submissions of AIGER model checkers we did not run a single safety property track using the AIGER format as in earlier competitions until 2017. Instead we were running model checkers only supporting the AIGER format on bit-blasted word-level models. This allowed to compare AIGER model checker directly with word-level model checkers, exept that we can not bit-blast arrays which puts AIGER model checker at a big disadvantage in the overall ranking.

Setup

The hardware setup was identical to the competition in 2019. It was running on our Ubuntu 18.04.5 LTS 64 bit cluster with two Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz CPUs and 128 GB of main memory on each node.

Each solver had 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 previous competitions we will further used a time limit of 1 hour of wall clock-time.

Submission

Email submissions to
"Armin Biere" <armin.biere@jku.at>,
"Nils Froleyks" <nils.froleyks@jku.at>, and
"Mathias Preiner" <preiner@cs.stanford.edu>.

Registration and first versions of model checkers were due on September 1.

It was possible to send updates of model checkers until September 8.

New benchmarks were accepted until September 8 as well.

All submission dates were anywhere on earth.

Organization

HWMCC'19 was organized by

Armin Biere, Johannes Keplers University Linz, Austria
Nils Froleyks, Johannes Keplers University Linz, Austria
Mathias Preiner, Stanford University, USA

History

HWMCC'19 at FMCAD'19, San Jose, USA
HWMCC'17 at FMCAD'17, Vienna, Austria
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