Affiliated to CAV'14
and FLoC'14 Olympic Games
HWMCC'13, HWMCC'12, HWMCC'11, HWMCC'10, HWMCC'08, and HWMCC'07.
This was the 7th competitive event for hardware model checkers.
Gödel medals were awarded to the best teams of each of the three tracks.
However, every team could only obtain one medal. Tracks are ranked by their importance, deep bound track first, single track second, liveness track last.
Deep Bound Track
Gödel medal and $500 check goes to TIP.
Single Safety Property Track
Gödel medal goes to ABC.
Gödel medal goes to IIMC.
The results were presented on the second day of the main part of CAV'14.
Medals and certificates were handed over in the second ceremony of the FLoC'14 Olympic Games on next to last day.
The benchmarks are available as hwmcc14benchmarks.7z.
Beside slides and log files we have:
We are working on making more material available soon.
Model checkers were required to produce witnesses for single safety properties. These traces were checked by the AIGSIM tool, which is part of the AIGER tools.
Otherwise, the competition was run almost the same way as in the previous two years, except that more powerful hardware was used.
The competition was run on a cluster at Aalto University, with exclusive access to 32 nodes of 2x Six-Core AMD Opteron 2435 2.6GHz with at least 16 GB of RAM. This meant 12 cores for each solver per benchmark, memory limit around 15 GB and time limit of 900 seconds.
Beside the requirement to produces witnesses, rules, input and output format did not change. Please consult the pages of HWMCC'12 for more details. The Oski benchmarks from 2013 which contained uninitialized latches were reencoded to conform to the pre AIGER 1.9 format. All benchmarks only have zero initialized latches.
There were three real silver medals handed out to the winners at the FLoC'14 Olympic Games ceremony in the second week.
Thus it was decided to only have three tracks: the single safety, the liveness and the deep bound track. There was no multiple property track for the CAV edition. It was technically the most challenging one and we only got three medals to hand out.
HWMCC'14 is organized by Armin Biere, JKU Austria, and Keijo Heljanko, Aalto University Finland.
We are grateful to Oski Technology, which again was sponsoring the deep bound track award.
The winner of the deep bound track got a medal and a check.
The competition was also sponsored by RiSE and Aalto Shool of Science.
First version of model checkers were due June 1 and updates of model checkers were possible until June 15.