We are preparing for the fifth annual reactive synthesis competition, which will again be affiliated with CAV, and will run in time for the results to be presented at CAV and SYNT, which are both part of the Federated Logics Conference (FLoC) 2018.

The competition will run mostly in the same way as in 2016 and 2017: there are main tracks for safety specifications in AIGER format and for LTL specifications in TLSF, each separated into subtracks for realizability checking and synthesis, and evaluated separately in sequential and parallel execution modes. Like last year, we supply the  synthesis format conversion tool SyFCo that allows to convert TLSF into several forms, including input formats of a number of existing synthesis tools. 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, both in AIGER and in TLSF. We accept new benchmarks at any time. New benchmarks can be included in SYNTCOMP 2018 if they are sent to us by June 1, 2018.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until May 25. As in previous years, we will allow updates of the solvers for some time after that (possibly after feedback from the organizers), at least until June 1. However, it would help the organizers to know in advance how many solvers may be entering, and who is seriously interested in entering SYNTCOMP. Thus, if you plan to enter one or more solvers into SYNTCOMP 2018, please let us know at your earliest convenience.

* 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, write to jacobs@react.uni-saarland.de.

On behalf of the SYNTCOMP team,

Swen