The 5th Syntax-Guided Synthesis Competition (SyGuS-Comp) will take place as a satellite event of FLoC, CAV and SYNT 2018.
UPDATE: SyGuS-Comp 2018 has concluded (Results). Congratulations to all winners.
|18 July 2018||Solvers presentation (at SYNT’18 workshop)|
Call for Participation
This is a call for participation in the 5th Syntax-Guided Synthesis Competition to be organized as a satellite event of SYNT and CAV 2018 and as part of the FLoC Olympic games.
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’18) 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 firstname.lastname@example.org.
This year’s competition will have 5 tracks:
- General SyGuS track (General),
- Invariant synthesis track (INV),
- Conditional Linear Integer Arithmetic track (CLIA),
- Programming By Examples [Strings] track (PBE-Strings), and
- Programming By Examples [Bit Vectors] track (PBE-BV).
See Specification Language for more details about these tracks.
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.
The scoring system is per track and as follows.
A solver that solved benchmarks in the track, out of which benchmarks among the fastest1, and benchmarks with an expression size among the smallest2 will receive a score: . The solver with highest score will be announced the winner of the track — an honor which will be accompanied by a FLoC 2018 Olympic games medal.
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.
Five solvers participated in SyGuS-Comp’18:
- CVC4 (in all 5 tracks)
Andrew Reynolds (University of Iowa), Haniel Barbosa (University of Iowa), Andres Notzli (Stanford University), Cesare Tinelli (University of Iowa) and Clark Barrett (Stanford University)
- DryadSynth (in INV and CLIA tracks)
KangJing Huang (Purdue University), Xiaokang Qiu (Purdue University) and Yanjun Wang (Purdue University)
- EUSolver (in all 5 tracks)
Arjun Radhakrishna (Microsoft) and Abhishek Udupa (Microsoft)
- Horndini (in INV track)
Deepak D’Souza (IISc, Bangalore), P. Ezudheen (IISc, Bangalore), P. Madhusudan (UIUC), Pranav Garg (Amazon), Daniel Neider (MPI-SWS) and Shubham Ugare (IIT, Guwahati)
- LoopInvGen (in INV track)
Saswat Padhi (UCLA), Rahul Sharma (Microsoft Research, Bangalore) and Todd Millstein (UCLA)
The winners for various tracks are as follows.
- PBE-BV Track: CVC4
- PBE-Strings Track: CVC4
- INV Track: LoopInvGen
- CLIA Track: CVC4 and DryadSynth
- General Track: CVC4