With SYNTCOMP 2016, we have the first major extension of the competition, from pure safety properties to full LTL. The new track is based on the TLSF format, and had 3 participants for the first competition. The AIGER-based safety track also still exists, and we had 3 completely new participants in that track also, in addition to 3 that have participated before.

The SYNTCOMP 2016 results have been presented at the SYNT workshop (slides) and are available on the web-frontend of our EDACC instance. An analysis of the results has been published in the proceedings of SYNT 2016.

Most notably, the following tools had the best results in some of the categories:

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

AbsSynthe (solved 181 out of 234 problems in the AIGER/safety Realizability Track, parallel mode, and 165 out of 2015 in the Synthesis Track, parallel mode)

SafetySynth (solved 153 out of 215 problems in the AIGER/safety Synthesis Track, sequential mode)

Acacia4Aiger (solved 153 out of 195 problems in the TLSF/LTL Realizability Track)

BoSy (solved 138 out of 185 problems in the TLSF/LTL Synthesis Track)

Many thanks to all contributors of benchmarks and all participants!