[HWMCC'20] Call for model checkers and benchmarks

[Armin Biere]

HWMCC'20

http://fmv.jku.at/hwmcc20/

Affiliated to FMCAD'20

https://fmcad.forsyte.at/FMCAD20/

September 22 - 24, 2020

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

Format

As introduced last year we will have 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.

Depending on the interest of the community we also consider to run a single safety property track using the AIGER format as in earlier competitions until 2017. Alternatively model checkers only supporting the AIGER format can run on bit-blasted word-level models.

Setup

The hardware setup is identical to the last competitions. 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" <armin...@jku.at>,

"Nils Froleyks" <nils.f...@jku.at>, and

"Mathias Preiner" <pre...@cs.stanford.edu>.

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

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

New benchmarks are accepted until September 8 as well.

All submission dates are anywhere on earth.

Organization

HWMCC'19 is organized by

Armin Biere, Johannes Keplers University Linz, Austria

Nils Froleyks, Johannes Keplers University Linz, Austria

Mathias Preiner, Stanford University, USA