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.
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.
Before the competition there was a qualification round.
Successful participation in the qualification round was mandatory to qualify.
Solvers are evaluated based on the number of instances solved and the total time needed.
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.