We are preparing for the annual reactive synthesis competition, which will run in time for the results to be presented at CAV 2023 and SYNT 2023. The competition will run mostly in the same way as in previous years. If you plan on submitting a benchmark or solver, please go to StarExec, create a user, and contact us to be added to the SYNTCOMP space. There are main tracks for safety specifications in AIGER format, for LTL specifications in TLSF, for parity games in extended HOA, and:

New this year: LTLf specifications in an extended version of the TLSF format! If you are interested, please contact us for more details on the exact semantics and the format we will be using for this track.

Each track is separated into subtracks for realizability checking and synthesis. 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 any of the formats (AIGER, TLSF, extended HOA). New benchmarks can be included in SYNTCOMP 2023 if they are correctly submitted to our benchmark repository by June 1, 2023. Please create a new issue, attach an archive with your new benchmarks with a sensible name, and make sure the archive should also contains 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. 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 2023 if it is correctly uploaded into StarExec by June 1, 2023.

* 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, guillermo.perez@uantwerpen.be, or philipp@lrde.epita.fr

Dear synthesis enthusiasts, for the next edition of the Reactive Synthesis competition (SYNTCOMP 2020) we will have a new track which is meant to further distinguish the strengths of LTL/TLSF synthesis tools. The new track will have as input deterministic parity automata, an intermediate representation for most LTL-synthesis pipelines.

The new input format is an extension of the Hanoi Omega-Automata (HOA) format. There exist Java and C++ parsers (see the website) for the original format and the extension is such that those parsers should work for it. Furthermore, for PGSolver-format fanatics we provide a translator from the new format to PGSolver format. The output format will remain AIGER, as explained in the arXiv document describing the input/output formats.

We encourage you to start preparing benchmarks and tools for this new track as soon as possible and to try them out in our StarExec community. If you have questions or comments regarding the input/output formats, do not hesitate to contact us.

New benchmarks in TLSF have been added to our benchmark repository. They include a decomposed version of the well-known AMBA benchmark, and unrealizable variants of the parameterized benchmarks from last year.

With SYNTCOMP 2016, we have the first major extension of the competition, from pure safety properties to full LTL. The new track is based on the TLSF format, and had 3 participants for the first competition. The AIGER-based safety track also still exists, and we had 3 completely new participants in that track also, in addition to 3 that have participated before.

The SYNTCOMP 2016 results have been presented at the SYNT workshop (slides) and are available on the web-frontend of our EDACC instance. An analysis of the results has been published in the proceedings of SYNT 2016.

Most notably, the following tools had the best results in some of the categories:

Simple BDD Solver (solved 175 out of 234 problems in the AIGER/safety Realizability Track, sequential mode)

AbsSynthe (solved 181 out of 234 problems in the AIGER/safety Realizability Track, parallel mode, and 165 out of 2015 in the Synthesis Track, parallel mode)

SafetySynth (solved 153 out of 215 problems in the AIGER/safety Synthesis Track, sequential mode)

Acacia4Aiger (solved 153 out of 195 problems in the TLSF/LTL Realizability Track)

BoSy (solved 138 out of 185 problems in the TLSF/LTL Synthesis Track)

Many thanks to all contributors of benchmarks and all participants!

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

SYNTCOMP 2015 will officially be a part of CAV 2015 and SYNT 2015.

We have updated our page with the schedule, rules, FAQ, and submission information for the second installation of the competition.

We are looking forward to your submissions of benchmarks and tools for this year’s competition!

Preparations for SYNTCOMP 2015 have started. The main tracks of the competition will be the same as this year (with modified evaluation rules), and the schedule will (presumably) also be similar:
– benchmarks can be submitted until End of April 2015
– tools can be submitted until End of May 2015
– after submission, tools will be tested, and we will allow re-submission in case of errors if time permits
– the competition will be finished until CAV 2015

Most importantly at this point, we are looking for more benchmarks for SYNTCOMP 2015. If you can supply us with benchmarks in AIGER format, you will be able to upload them directly to our EDACC-system soon. If you have an interesting benchmark set that still needs to be translated, please let us know.

More details on SYNTCOMP 2015, and a full archive of the data produced at the first competition, will be released soon.

The deadline for submission of synthesis tools for SYNTCOMP 2014 has passed, and we are now starting testing in the competition environment. We are happy to say that we have submissions of a good number of solvers from 6 different research groups.

We are willing to accept last minute entrants if they run without major problems in our environment (and of course, submitted tools can still be re-submitted during the next 2-3 weeks under the same condition). Please contact me (swen.jacobs@iaik.tugraz.at) if you still want to submit a tool.

We found and fixed bugs in the reference implementation supplied with the testing framework for SYNTCOMP (here). We will however not update the package. Instead, please download the latest version from Bitbucket (to update, simply replace aisy.py from your installation with the one from the repository).

As of today, the benchmark set for SYNTCOMP 2014 is fixed. Overall, we have collected 6 sets of benchmarks, with more than 500 individual synthesis problems. The benchmarks are available in our Bitbucket repository on the Synthesis Competition Server (after registration). Of course we still welcome new benchmarks, but they will not be used in the 2014 competition anymore.

Solver submission for 2014 is open on the same server. If you are developing a synthesis tool for the competition, please have a look at the reference implementation and testing framework, and submit a first version of your tool until End of May 2014.