HWMCC'11

Results

The slides of the presentation have additional information.

Single-Property

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:

ALL	SuperProve	University of California, Berkeley
SAT	SimpleBIP	University of California, Berkeley
UNSAT	SuperProve	University of California, Berkeley

More detailed ASCII tables for the single track are available too.

A flat excel spread sheet (ASCII) with results on all single benchmarks is also available.

There is also a joined excel spread sheet (ASCII) which has all single results joined per benchmark on one line.

Even more details are in the single-logs.7z archive of all single log files.

Liveness

We also had some first experience with liveness properties.

The winners in the live track are:

ALL	TIP	Chalmers University, Göteborg
SAT	TarmoBMC	Aalto University, Helsinki
UNSAT	IIMC	University of Colorado, Boulder

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.

A flat spread sheet (ASCII) with results on all live benchmarks is also available.

There is also a joined excel spread sheet (ASCII) which has all live results joined per benchmark on one line.

Even more details are in the live-logs.7z archive of all live log files.

Multi-Property

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:

ALL	Tarmo	Aalto University, Helsinki
SAT	Tarmo	Aalto University, Helsinki
UNSAT	Tarmo	Aalto University, Helsinki

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.