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

This year, the competition will run with a new setup! Besides continuing to use the TGCC (https://www-hpc.cea.fr/tgcc-public/en/html/tgcc-public.html), we accept solvers in a rolling fashion. We will freeze the working versions July 1, but please send your (updated) solvers at any point.

Solver submission: To submit your solvers, things will be simplified to the creation of a docker image with your solver and you communicating to the organizers the repository address of the image.

In SYNTCOMP 2026, we will run the following tracks (based on the same rules and with the
same specification formats as in previous years):
– realizability and synthesis for LTL specifications in TLSF
– realizability for parity games in extended HOA and
– realizability for LTLf specifications in an extended version of the TLSF format.

Tools will be evaluated with respect to the number of solved benchmarks, and (for
synthesis) with respect to the size of their solutions.

Call for Benchmarks

We are looking for new synthesis benchmarks to include into SYNTCOMP, in any of the formats (TLSF, extended HOA). New benchmarks can be included in SYNTCOMP 2026 if they are correctly submitted to our benchmark repository https://github.com/SYNTCOMP/benchmarks by June 1. Please create a new issue, attach an archive with your new benchmarks with a sensible name, and make sure the archive should also contain a readme.md or readme.pdf describing the benchmarks, relevant papers, etc. We will check if everything is OK, and then add it to the repository. Alternatively, you can create a pull request with your benchmarks.

Call for Solvers

Solvers for all tracks of the competition will be accepted until June 1. Your solver will
be included in SYNTCOMP 2026 if:
– the address of a working docker extension is communicated to us by June 1, and
– a technical description of the solver is submitted with it. (A pdf of 1-2 pages in LNCS
format please.)

Please use this docker image as the basis for your submission and contact us as soon as possible so that we can start testing it in the cluster. This is especially important if you prefer that we compile your tool in the server!

If you are interested in submitting a solver, please have a look at the pages for Rules, Schedule, Submission, and FAQ on https://www.syntcomp.org/. If you have any further questions or comments, please write to jacobs@cispa.de, guillermo.perez@uantwerpen.be, and philipp.schlehuber-caissier@telecom-sudparis.eu.