TLSF v1.1

We have just published a small update to the temporal logic synthesis format (TLSF). The main changes are:

  • additional sections for initial properties of environment and system, and for invariant properties of the environment (these have also been renamed, but the old names are still supported), and
  • support for user-defined enumeration types.

The changes are described in the new TLSF format description, and are supported by the first release of the synthesis format conversion tool (SyFCo).

The rules and call for benchmarks and solvers pages have been updated accordingly.

SYNTCOMP 2016: Call for Benchmarks and Solvers

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: Results

SYNTCOMP 2015 has been another big success, as witnessed by a greatly extended benchmark library and impressive improvements in most of the participants. The results have been presented at the SYNT workshop (slides) and are available on the web-frontend of our EDACC instance.

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

Simple BDD Solver (solved 195 out of 250 problems in the Realizability Track)

AbsSynthe (solved 161 out of 239 problems in the Synthesis Track, sequential mode)

Demiurge (solved 180 out of 239 problems in the Synthesis Track, parallel mode)

Many thanks to all contributors of benchmarks and all participants!

Synthesis Competition 2014: Results

(This post replicates information that was previously included on the front page of this site. It does not contain new information, except for a link to the written report on arXiv and STTT)

SYNTCOMP 2014 was a big success: 5 synthesis tools competed in 4 different categories, crunching on the 569 benchmark instances we collected for the first competition. The results have been presented at CAV (slides) and the SYNT workshop (slides). The written report, including descriptions of the benchmarks, tools, and results, is available on arXiv.
Update: the report for SYNTCOMP 2014 has now appeared in STTT (Software Tools for Technology Transfer).

The winners of the 4 tracks are:

Synthesis (Sequential):
AbsSynthe from R. Brenguier, G.A. Pérez, J.-F. Raskin, O. Sankur (UL de Bruxelles)

Synthesis (Parallel):
Demiurge from R. Könighofer (TU Graz), M. Seidl (JKU Linz)

Realizability (Sequential):
Simple BDD Solver from L. Ryzhyk (University of Toronto, NICTA) and A. Walker (NICTA)

Realizabiltiy (Parallel):
Basil from R. Ehlers (University of Bremen, DFKI Bremen)

As part of the FLoC Olympic Games, every track winner received a Kurt Gödel medal in silver, handed over by Ed Clarke:

VSL 2014_by_Nadja Meister_IMG_1377
(f.l.t.r.: Leonid Ryzhyk, Rüdiger Ehlers, Ed Clarke, Guillermo A. Pérez, Martina Seidl, Swen Jacobs, Thomas Krennwallner)
(c) VSL / Nadja Meister

Detailed information on the first competition can be found here. If you are interested, you can have a look at our rules, and download a testing framework that contains a simple reference implementation of a synthesis tool that handles the competition format, along with a set of benchmarks and a model checker to verify results.

Benchmark collection for 2015 finished

We have finished collecting benchmarks for SYNTCOMP 2015. Joining the 569 benchmark instances from last year are more than 2000 new benchmark instances, including new and challenging instances of existing benchmarks and 6 completely new sets of benchmarks.
We are currently working hard on testing and categorizing the benchmarks, and coming up with a scheme for selecting benchmarks for the competition (with the goal to have a good distribution across benchmarks from different problem sets and of different difficulty).

For testing purposes, the preliminary set of new benchmarks is available in folder Benchmarks2015 of our Bitbucket repository. Note that some of the files still contain errors (like 2 instead of 1 outputs), and many of them are very hard and have not been solved by any of the tools from last year in our test runs.

SYNTCOMP 2015: Preliminary Schedule, Call for Benchmarks

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.

Testing Phase started, Submission of Last-Minute Entrants

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.

Benchmark Collection for 2014 finished, Solver Submission open

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.