HWMCC'11

The main single safety/bad-state property track used exactly the same AIGER format as previous competitions.

New Format

In order to participate in the mulit-property-track or in the liveness-track a model checker had to be able to read AIGER models in the new 1.9 format.

We have a draft on the differences of the new version of the AIGER format compared to the old format. We did not enforce strict conformance to the output format for witnesses during the competition.

Beginning with version 1.9.1 of AIGER new features of this draft have been implemented in the AIGER library. Submitters had been encouraged to and also did use the new AIGER library to read the new format even though the extensions should have been easy to implement in existing pre 1.9 AIGER parsers.

A first set of benchmarks translated into the new AIGER 1.9 format by Siert Wieringa was made available before the competition.