We are preparing for the annual reactive synthesis competition, which will run in time for the results to be presented at CAV 2020 and SYNT 2020.

The competition will run on StarExec, as in 2019. If you plan on submitting a benchmark or solver, please go to https://www.starexec.org/, create a user,
and contact us (jacobs@cispa.saarland, guillermoalberto.perez@uantwerpen.be) to be added to the SYNTCOMP space. There are main tracks for
– safety specifications in AIGER format,
– LTL specifications in TLSF, and
– a new track for parity games in Hanoi Omega-Automata (HOA) format,
each separated into subtracks for realizability checking and synthesis, and
into sequential and parallel execution modes. Tools will be evaluated with respect to the number of solved benchmarks, and with respect to the size of their solutions.

* Call for Benchmarks *

We are looking for new synthesis benchmarks to include into SYNTCOMP, in AIGER, TLSF, and HOA. New benchmarks can be included in SYNTCOMP 2020 if they are correctly uploaded (i.e. pass syntax checks) into StarExec by June 1, 2020. Contact us (see above) if you have any questions regarding scope or format of benchmarks.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until June 1. Because of our move to StarExec, you will be allowed to update your solver as many times as needed. Your solver will be included in SYNTCOMP 2020 if it is correctly uploaded (i.e. passes a test run) into StarExec by June 1, 2020.

* Communication *

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ. If you have any further questions or comments, please write to jacobs@cispa.saarland and guillermoalberto.perez@uantwerpen.be