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

This year, the competition will run with a new setup!

From 2025 onward, the competition will be run on the French Très Grand Centre de Calcul
du CEA (TGCC), https://www-hpc.cea.fr/tgcc-public/en/html/tgcc-public.html. 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 2025, 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 2025 if they are correctly submitted to our benchmark repository https://github.com/SYNTCOMP/benchmarks by June 1, 2025. 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 2025 if:
– the address of a working docker extension is communicated to us by June 1, 2025, and
– a technical description of the solver is submitted with it. (A pdf of 1-2 pages in LNCS
format please.)
A docker image that should be used as the basis of your submission will be made available
in the next 2-3 weeks.

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.