Rules

The competition is still in its infancy.

Thus we focus on attracting as many benchmarks and model checkers as possible.

Rules are not applied strictly.

Input and Output Format

The input and output format requirements are described in the AIGER format report.

We are currenlty extending the format to model liveness through generalized Büchi-Automata.

In case you have benchmarks and model checkers for liveness, more specifically, fair loop detection, please contact the organizers.

Another direction is to include word-level model checkers as well.

Execution Environment

• Operating System: Ubuntu Linux 7.10
• Processor: Intel Pentium 4, 3 GHz
• Memory: 2 GB (1.5 GB memory limit enforced)
• Cache: 1024 KB
• Compiler: GCC 4.1.3

Qualification Round

Before the competition there was a qualification round.

Successful participation in the qualification round was mandatory to qualify.

Assessment of Solvers

Solvers are evaluated based on the number of instances solved and the total time needed.

Prizes

Restrictions

Due to limited computational resources, the organizers reserve the right not to accept more than 4 different model checkers from the same organization.

The organizers also reserve the right to submit their own systems — or other systems of interest — to the competition.