SyGuS-Comp 2017: Results and Analysis

Rajeev Alur
(University of Pennsylvania)
Dana Fisman
(Ben-Gurion University)
Rishabh Singh
(Microsoft Research, Redmond)
Armando Solar-Lezama
(Massachusetts Institute of Technology)

Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula phi in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB.

The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition six new solvers competed on over 1500 benchmarks. This paper presents and analyses the results of SyGuS-Comp'17.

In Dana Fisman and Swen Jacobs: Proceedings Sixth Workshop on Synthesis (SYNT 2017), Heidelberg, Germany, 22nd July 2017, Electronic Proceedings in Theoretical Computer Science 260, pp. 97–115.
Published: 28th November 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: