SyGuS-Comp 2017: Results and Analysis
Rajeev Alur (1), Dana Fisman (2), Rishabh Singh (3), Armando, Solar-Lezama (4) ((1) University of Pennsylvania, (2) Ben-Gurion University,, (3) Microsoft Research, Redmond, (4) Massachusetts Institute of Technology)
TL;DR
This paper reports on the results and analysis of the 2017 Syntax-Guided Synthesis Competition, evaluating various solvers on a large benchmark set to advance research in program synthesis.
Contribution
It provides a comprehensive evaluation of six new solvers for SyGuS on over 1500 benchmarks, highlighting progress and challenges in the field.
Findings
Six new solvers competed on over 1500 benchmarks
Analysis of solver performance and effectiveness
Insights into current state and future directions of SyGuS research
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 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.