Author Archives: Swen Jacobs

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.