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).
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.
FLoC’14 Olympic Games
SYNTCOMP will be a part of the FLoC’14 Olympic Games. The winners in the competition categories will be awarded Kurt Goedel medals (in silver) at the FLoC Olympic Games award ceremonies. Details to be announced.
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 benchmark repository
The ExCape Project, with our sister competition on functional/software synthesis.