HWMCC’24

This will be the 12th competitive event for hardware model checkers.

Affiliated to FMCAD’24

October 14 - 18, 2024, Prague, Czech Republic

Format

This year we will have three tracks with single safety properties:

1. Word-level without arrays
2. Word-level with arrays
3. Bit-level with mandatory safety certificates

Note that for 3) we will translate the word-level benchmarks from 1) and 2) to AIGER bit-level benchmarks. The certificate will be checked with Certifaiger.

As in previous years, the word-level track is based on the BTOR2 format, which is described in BTOR2 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.

Setup

TBD

Benchmarks

Submission deadline for new benchmarks is August 18, 2024. Please submit your benchmarks in BTOR2 format. If benchmarks have multiple safety properties, we’ll split them up in separate benchmarks with one safety property each.

Submission

Please send model checker and benchmarks submissions to

• Armin Biere
• Nils Froleyks
• Mathias Preiner

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

All submission dates are anywhere on earth (AoE).

Organization

HWMCC’24 is organized by

• Armin Biere, University of Freiburg, Germany
• Nils Froleyks, Johannes Keplers University Linz, Austria
• Mathias Preiner, Stanford University, USA