Since the last competition in 2007 was the first of its kind and we wanted to attract as many benchmarks and model checkers, the rules were not applied strictly. This will change next year.
Adherence to the input and output format will be required. At most one solver of each group will be allowed in the final run of each category. Splitting the model checkers into a demonstration and competition devision may also be option.
The input and output format requirements are described in the AIGER format report. We are actively working on extending the format to model liveness through generalized Büchi-Automata. Another idea is to include word-level model checkers as well.
Before the competition there will be a qualification round.
Successful participation is mandatory to qualify.
Solvers will be evaluated based on the number of instances solved and the total time needed.