The slides of the presentation have additional information.
The simple safety checking track used the old AIGER format.
Each benchmark had exactly one output, interpreted as bad state property.
Thus this track had exactly the same rules and input format as in previous competitions.
The winners of the single track are:
More detailed ASCII tables for the single track are available too.
Even more details are in the single-logs.7z archive of all single log files.
We also had some first experience with liveness properties.
The winners in the live track are:
After the competition we realized that the original IIMC submitted to the competition did not handle justice properties properly depending combinationally on inputs (kind of Mealy-style justice properties). It was assumed, that justice properties only depend on latches directly.
This lead to wrong answers of the original version of IIMC for 5 instances from the arbiter series submitted by Koen Claessen.
arbi0s08p03 arbixs08p03 arbixs16p03 arbixs32p03 arbixs64p03
By construction these instances were supposed to be unsatisfiable, but IIMC claimed satisfiability without providing a witness. Since nobody else solved these instances, IIMC scored these 5 instances.
The authors of IIMC fixed the problem and the fixed version of IIMC times out on these 5 instances and in addition on 3 satisfiable instances from this series:
arbixs16bugp03 arbixs32bugp03 arbixs64bugp03
Therefore the fixed IIMC scores 8 instances less. Otherwise there was no change in the scores. This also did not affect the single track.
As a consequence the SAT+UNSAT ranking in the liveness track changed by IIMC and TIP switching positions. TIP became overall winner of the liveness track. There is no change in the UNSAT ranking in this track, where IIMC still shows remarkable strength.
We have only added this change to the ASCII tables for the live track. The other files below in the liveness track do not include references to the runs of the fixed IIMC.
More detailed ASCII tables for the live track are available too.
Even more details are in the live-logs.7z archive of all live log files.
With HWMCC'11 we started to use models with multiple properties, actually only again simple safety/bad-state properties.
The results are mixed, but there is (actually only) one winner:
More details for the multi property are only available in rather preliminary form as multi-details-table.txt. PdTrav is assumed not to have worked correctly in combination with environment constraints in the multi-properties version.
We do not have further spread sheets for the multi track as in the other tracks.
Even more details are in the multi-logs.7z archive of all multi log files.