The competition consisted of a single safety property track (SINGLE), a (single) liveness property track (LIVE), and a deep bound track (DEEP), but no multiple property track. The winner of the deep bound track received an award of $500 sponsored by Oski Technology.
The tracks were runnnin in the same way as in the previous four incarnations of the competition, except that we used our new cluster running Ubuntu 16.04.2 64 bit. Each cluster node had two Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz CPUs and 128 GB of main memory.
Each solver had 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 was enforced. As in the previous competition in 2015 we further used a time limit of 1 hour of wall clock-time.
Also as before the number of submissions was restricted to at most two model checkers per submitter and model checkers were required to produce witnesses in the SINGLE track. These witnesses were checked by the AIGSIM tool, which is part of the AIGER tools.
Except for the new hardware, competition rules, as well as input and output formats did not change. Please consult the pages of previous competitions (see for instance HWMCC'12 or below) for more details.
Again as in 2014 and 2015, in order to avoid glitches in interpreting the format, the SINGLE track only used AIGER pre 1.9 single property benchmarks, with the single bad state property encoded as an output (MILOA header with O = 1). All latches were implicitly initialized to zero as it was the default in the pre 1.9 AIGER format.
There was no change in the LIVE track nor in the DEEP track. Solvers intended to participate in the DEEP track were run in the SINGLE track and were expected to print reached bounds as in previous years (see for instance HWMCC'12).