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 multiple properties and 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.
Solvers are evaluated based on the number of instances solved and the total time needed.
Due to limited computational resources, the organizers reserved the right not to accept more than 4 different model checkers from the same organization.
The organizers also reserved the right to submit their own systems — or other systems of interest — to the competition.