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.

Call for Benchmarks, Server for Competition 2014 Open

We have just opened the server for SyntComp 2014. It is based on the EDACC-framework, which is also used for the SAT competitions.

Most importantly at this point, we are looking for more benchmarks. These can directly be uploaded to the EDACC-system, which will also be used to run the competition itself. Upon registration, you are able to upload benchmarks, and also download all the benchmarks that have already been converted to the competition format. See the Call for Benchmarks for details.

Furthermore, the same account allows you to upload synthesis tools. If they compile on our competition cluster, they can enter SyntComp 2014. Official submission of tools will be in May 2014. See the rules and the submission page for details.

Introducing the SyntComp Format (v0.1)

Today we present the result of our open discussions up to and
including at the SYNT workshop, and some internal discussions
afterwards.

Basic Format

We think that, in order to have a successful competition at CAV/SYNT
2014, the three most important things are: i) keeping the format
simple, ii) having sufficiently many competing tools, iii) supplying
the community with a format, benchmark set and framework for testing
their tools as early as possible.

These three points led us to choosing the AIGER format — restricted to
safety specifications, like in the main category of the HWMCC — both
as input and ouput format for the synthesis competition. For the input
format, we need to add a partition of inputs into controllable and
uncontrollable, but otherwise we can build on a
well-known language with a clear semantics and existing tool
support. For the output format, choosing AIGER allows us to almost
directly check the synthesized artifacts with any model checker that
supports the format (in particular, any that competes in the HWMCC). A
description of how we plan to use the AIGER format in
reactive synthesis can be found here: Format Proposal (v0.1).

In the coming weeks, we will be working on
i) converting as many benchmarks as possible to the AIGER format, with
bounded approximation of liveness properties by safety properties
ii) implementing a framework that allows potential participants to
adapt their tools to the new in- and ouput format, and test them in
an environment that resembles that of the competition itself
iii) developing a formal description of the format and a detailed
ruleset for the competition.

Extended Format

The discussions in St. Petersburg made clear that there is an interest
in more expressive specifications, like full LTL. There are a number
of additional problems to be solved for supporting this in the
competition. Most importantly, on the one hand LTL poses a rather high
entry barrier, even with existing tools for conversion to different
automata formats, and on the other hand we cannot expect the resulting
artifacts to be verified formally by existing model checkers. Thus, it
will be much more difficult to assess and rank
solutions. Still, we are thinking about how we could include a full
LTL track into the competition, and are open to suggestions on how to
best achieve this.

As always, questions, comments, and suggestions are very welcome!

Synthesis Competition(s) at CAV 2014

This is the first post on SyntComp.org! In the future, SyntComp.org will report news and host discussions about the synthesis competition. We begin with the announcement that there will be competitions for both functional and reactive synthesis at CAV 2014. We are currently figuring out the details and will keep you updated and ask for your opinion right here.

Content will be added to this page in the coming days and weeks. For now, here is a list of imporant links:

The SyntComp mailing list

The SyntComp benchmark repository

The ExCape Project, with our sister competition on functional/software synthesis.