Hardware Model Checking Competition


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

Affiliated to FMCAD’24

October 14 - 18, 2024, Prague, Czech Republic


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.




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.


Please send model checker and benchmarks submissions to

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

All submission dates are anywhere on earth (AoE).


HWMCC’24 is organized by