The results of SYNTCOMP 2017 have been presented at the SYNT workshop and at CAV 2017, and the experiments can be inspected in the web-frontend of our EDACC instance. An analysis of the results has been published in the proceedings of SYNT 2017.

Like in the previous years, the competition was split into a safety track, based on specifications in AIGER format, and an LTL track, with specifications in TLSF. In each of the tracks, we consider the different tasks of realizability checking and synthesis, and split evaluation into sequential and parallel execution modes. Finally, for the synthesis tasks we have an additional ranking based on not only the quantity, but also the quality of solutions.

Here are the tools that had the best results in these categories:

Simple BDD Solver (solved 171 out of 234 problems in the AIGER/safety Realizability Track, sequential mode)

TermiteSAT (solved 186 out of 234 problems in the AIGER/safety Realizability Track, parallel mode)

SafetySynth (solved 155 out of 234 problems in the AIGER/safety Synthesis Track, sequential mode, and won the quality ranking in that mode with 236 points)

AbsSynthe (solved 169 out of 2015 in the AIGER/safety Synthesis Track, parallel mode)

Demiurge (won the quality ranking in the AIGER/safety Synthesis Track, parallel mode, with 266 points)

Party (solved most problems in all TLSF/LTL tracks and modes, and won the quality ranking in the TLSF/LTL Synthesis Track, parallel mode, with 308 points)

BoSy (won the TLSF/LTL Synthesis Track, sequential mode, with 298 points)

Congratulations to the winners, and many thanks to all contributors of benchmarks and all participants!