HWMCC Logo

HWMCC'19


Google Group





sponsors

Oski


JKU



FWF

[ results | tables | logs | benchmarks | awards | setup | submission | organization | previous editions ]

HWMCC'19

Affiliated to FMCAD'19

October 22 - 25, 2019

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

The slides for presenting the competition results at FMCAD'19:

[ HWMCC19-talk.pdf ]

Results

In the SINGLE bit-vector track the top three places are:
  1. AVR
    Aman Goel, Karem Sakallah (University of Michigan)
  2. CoSA2
    Makai Mann, Ahmed Irfan, Florian Lonsing, Clark Barrett (Stanford University)
  3. CoNPS-btormc-THP
    Norbert Manthey (hobbyist, former postdoc @ TU Dresden)
In the SINGLE bit-vector+array track the top three places are:
  1. CoSA2
    Makai Mann, Ahmed Irfan, Florian Lonsing, Clark Barrett (Stanford University)
  2. AVR
    Aman Goel, Karem Sakallah (University of Michigan)
  3. CoNPS-btormc-THP
    Norbert Manthey (hobbyist, former postdoc @ TU Dresden)

Oski Award

CoSA2 for solving the largest number of benchmarks overall.

Benchmark Contribution Award

Clifford Wolf for contributing 3478 SINGLE benchmarks.

Tables

[ single-bv.txt | single-bv-sat.txt | single-bv-unsat.txt | single-bv.csv ]
[ single-array.txt | single-array-sat.txt | single-array-unsat.txt | single-array.csv ]
[ single-overall.txt | single-overall-sat.txt | single-overall-unsat.txt ]

Generated with zummarize.c from the following logs.

Logs

[ hwmcc19-single-logs.tar.xz ]

Benchmarks

[ hwmcc19-single-benchmarks.tar.xz ]

Format

This year our focus is on introducing 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.

Since this year will be the first time with an experimental word-level track there will be no declared winners.

Benchmarks

For testing purposes, participants can test their model checkers on the BTOR2 BEEM benchmarks. More information on these benchmarks can be found here.

Awards

An award of $1000 sponsored by Oski Technology will go to the model checker which solved the largest number of benchmarks.

Another symbolic award will go the submission which contributed most to the competition in terms of providing interesting benchmarks.

The organizers are not eligible for any of the awards.

Setup

The hardware setup is identical to the last competition. It is running on our Ubuntu 18.04.3 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 has 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 competition in 2017 we will further use a time limit of 1 hour of wall clock-time.

Submission

Email submissions to "Armin Biere" <biere@jku.at> and "Mathias Preiner" <preiner@cs.stanford.edu>.

Registration and first versions of model checkers are due on September 28 October 4.

It is possible to send updates of model checkers until October 13.

New benchmarks are accepted untli October 13 as well.

All submission dates are anywhere on earth.

Organization

HWMCC'19 is organized by

Armin Biere, Johannes Keplers University LInz, Austria
Mathias Preiner, Stanford University, 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