Affiliated to FMCAD'13,
Portland, OR, USA,
October 20-23, 2013.
This was the 6th competitive event for hardware model checkers.
Results were presented on Tuesday, 22nd October 2013,
The deep bounds track
award of $500 sponsored by
was awarded to TIP by Niklas Sörensson and Koen Claessen.
Please refer to the slides of the presentation
for a general overview on the results.
Here are spread sheets with more details:
[ hwmcc13-single-results-table-per-instance.csv ]
[ hwmcc13-single-results-table-per-solver.csv ]
[ hwmcc13-live-results-table-per-instance.csv ]
[ hwmcc13-live-results-table-per-solver.csv ]
[ hwmcc13-multi-results-table-per-solver-and-property.csv ]
[ hwmcc13-multi-results-table-per-solver-and-benchmark.csv ]
[ hwmcc13-multi-results-table-per-solver-and-benchmark.xls ]
Log files are available too, but will explode in space during decompression:
[ hwmcc13-single-logs.7z ] (5 MB compressed, 298MB uncompressed)
[ hwmcc13-live-logs.7z ] (2 MB compressed, 80 MB uncompressed)
[ hwmcc13-multi-logs.7z ] (57 MB compressed, 19 GB = 18883 MB uncompressed)
For the deep bounds track we have the following tables:
[ hwmcc13-bounds-unsolved-table.csv ]
[ hwmcc13-bounds-unsolved-table-with-score.xls ]
The set of benchmarks used in HWMCC'13
as archive hwmcc13aigs.7z (74 MB compressed, 373 MB uncompressed). It
lacks 24 Intel benchmarks used in the single track due to license
restrictions. Those have to be obtained separately.
The competition was run in the same
way as last year, except that
we continued to work on obtaining more
word-level models in our
BTOR format in order to add a word-level track in the future.
- Intentions to submit were due September 13, 2013.
- New benchmarks are accepted any time (even after the competition).
- For submission or any other request send EMail to firstname.lastname@example.org.
- Final versions of model checkers were due on September 20, 2013.
For more information see also our
HWMCC'13 was organized by
Martina Seidl, and