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 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.

Execution Environment

  • Operating System: Ubuntu Linux
  • Processor: Intel Quad Core, 2.6 GHz
  • Memory: 8 GB (7 GB memory limit enforced)
  • Time: limited to 900 seconds

Assessment of Solvers

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


Prized are awarded in three different categories, SAT, UNSAT, and ALL.


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.