SyGuS-Comp 2014

The 1^st Syntax-Guided Synthesis Competition (SyGuS-Comp) took place as a satellite event of FLoC, CAV and SYNT 2014.

Evaluation

Solvers are evaluated on the StarExec platform, which provided 200 dual quad-core machines with 256GB memory each. The solvers are run with a TIMEOUT value as well. The solvers were compared against 250 benchmarks and the scores were based primarily on the number of benchmark solved and the solving time, and secondarily on the succinctness of the synthesized solution.

Participating Solvers

Five solvers participated in SyGuS-Comp’14:

• Alchemist
  Pranav Garg (UIUC), Shambwaditya Saha (UIUC) and P. Madhusudan (UIUC)
• Enumerative
  Abhishek Udupa (University of Pennsylvania)
• Sketch
  Rishabh Singh (Massachusetts Institute of Technology), Armando Solar-Lezama (Massachusetts Institute of Technology)
• Stochastic
  Mukund Raghothaman (University of Pennsylvania)
• Symbolic
  Garvit Juniwal (University of California at Berkeley)

Results

The winner of the competition was the Enumerative (CEGIS) solver.

A detailed final report is available here.