Setup

900 seconds wall clock time limit, 7 GB memory limit.

32 node cluster, Intel Quad Core 2.6 GHz processors, 8 GB, Ubuntu 12.04.

Each solver has full access to one node (4 cores).

Working-directory = home-directory on NFS, /tmp/ for temporary files.

Output should go to stdout or stderr.

Deep Bounds Award

The Deep Bounds Award of $500 was sponsored by Oski Technology for the largest sum of maximum reached bounds by a solver in the single safety property track.

The solver should print a bound reached as soon it has determined that the bad state can not be reached up to and including that bound.

As soon the solver determines that the initial state is not bad it should print:

u0

Please use fflush to make sure the output is printed.

If the bad state is reachable at bound 4 the output should be:

u0
u1
u2
u3
1
b0
...

Not being able to prove any bound within the time limit counts as maximum bound 0 reached.

Proving that the initial state does not contain a bad-state counts as maximum bound 1 reached etc.

We only used instances which were not solved by any solver in the single property track. Only solvers which did not give any incorrect answers were considered for determining the set of unsolved instances.

Model checkers of the competition organizers run hors concours and can not receive the award.

Model checkers shown to provide incorrect answers in the single safety track are not considered for the award either.