Abstract

Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation (f) that meets both a semantic constraint given by a logical formula (\varphi) in a background theory (\mathbb{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 the SyGuS input format (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 the 5^th SyGuS-Comp, five solvers competed on over $1600$ benchmarks across various tracks. This paper presents and analyses the results of this year’s (2018) SyGuS competition.

BibTeX Citation

@article{corr18/alur/syguscomp,
  title         = {SyGuS-Comp 2018: Results and Analysis},
  author        = {Rajeev Alur and
                   Dana Fisman and
                   Saswat Padhi and
                   Rishabh Singh and
                   Abhishek Udupa},
  journal       = {CoRR},
  volume        = {abs/1904.07146},
  year          = {2019},
  eprint        = {1904.07146},
  archivePrefix = {arXiv},
  primaryClass  = {cs.PL},
  url           = {http://arxiv.org/pdf/1904.07146.pdf}
}