Monthly Archives: February 2023

SYNTCOMP 2023: Call for Solvers and Benchmarks

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