Affiliated to FMCAD'20
September 21 - 24, 2020
This was the 11th competitive event for hardware model checkers.
The slides summarizing the
results and presented in the HWMCC session
at FMCAD are
available as hwmcc20slides.pdf.
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.
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.
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.
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.
HWMCC'19 was organized by
HWMCC'19 at FMCAD'19, San Jose, USA