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

We have a major extension of the competition this year: in addition to safety specifications in AIGER format, we will have tracks for synthesis from temporal logic specifications in LTL and GR(1). Check out the description of the temporal logic synthesis format (TLSF) if you are interested in submitting a solver or benchmarks in the new format. We also supply the  synthesis format conversion tool SyFCo that allows to rewrite the new format into several forms, including input formats of a number of existing synthesis tools.

* 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 2016 if they are sent to us by April 30, 2016.

* Call for Solvers *

Solvers for all tracks of the competition will be accepted until May 21 (initial version), with a possibility to update the solver until May 31 (possibly after feedback from the organizers). 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 2016, 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