SyGuS-Comp 2016

The 3rd Syntax-Guided Synthesis Competition (SyGuS-Comp) will take place as a satellite event of CAV and SYNT 2016.

UPDATE: SyGuS-Comp 2016 has concluded (Results). Congratulations to all winners.

Important Dates

30 May 2016 Deadline for submitting benchmarks
14 June 2016 Deadline for submitting solvers and their descriptions
28 June 2016 Start running competition jobs on StarExec
14 July 2016 Notification of results to authors
17 July 2016 Solvers presentation (at SYNT’16 workshop)

Call for Participation

This is a call for participation in the 3rd Syntax-Guided Synthesis Competition to be organized as a satellite event of SYNT and CAV 2016.

There has been a lot of recent interest in both using SyGuS solvers for various synthesis applications and developing different solving algorithms. The SyGuS competition (SyGuS-Comp’16) will allow solvers to compete on a large collection of benchmarks and advance the state-of-the-art for program-synthesis tools. We invite authors to submit their SyGuS solvers to this year’s SyGuS Competition.

For questions regarding the competition please contact the organizers at sygus-organizers@seas.upenn.edu.

Competition Tracks

This year’s competition will have 4 tracks:

See Specification Language for more details about these tracks.

Evaluation

Solvers will be evaluated on the StarExec platform, which provided 200 dual quad-core machines with 256GB memory each. The solvers would be run with a TIMEOUT value. The SyGuS-correctness checker, as well as the solvers from last year’s competition are available on the SyGuS community at StarExec. Candidate participants are invited to register on StarExec, where they can easily compare their solvers to the previous ones against the public benchmarks.

Tool Submission and Description

We expect tool developers to test their solvers on the public benchmarks, and submit the solver binaries on StarExec by the solver submission deadline. Each solver submission should also be accompanied by a brief (1 – 2 page in IEEE format) description of the key ideas of the solver.

Licensing of Tools and Benchmarks:

All benchmarks will be made public after the competition. We encourage the tool developers to make their solvers open-source, but participants are welcomed to submit binaries of proprietary tools as well.

Participating Solvers

Nine solvers participated in SyGuS-Comp’16:

Results

The winners for various tracks are as follows.

Slides for final presentation of solvers: ICE-DT

A detailed final report is also available here.