Monthly Archives: July 2015

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.