The results of SYNTCOMP 2018 have been presented at the SYNT workshop and at FLoC 2018, and the slides of the SYNT presentation can be found here. The experiments can now be browsed on the web-frontend of our EDACC instance (experiments with “Legacy” in the name are based on older solvers running on this year’s benchmarks), and a more detailed analysis of the results is forthcoming.

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 165 out of 234 problems in the AIGER/safety Realizability Track, sequential mode)

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

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

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

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

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

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