SyGuS-Comp 2016: Results and Analysis

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 we added a new track devoted to programming by examples. This track consisted of two categories, one using the theory of bit-vectors and one using the theory of strings. This paper presents and analyses the results of SyGuS-Comp'16.

In Proceedings SYNT 2016, arXiv:1611.07178. arXiv admin note: text overlap with arXiv:1602.01170

References in corpus (3)

• Language to Specify Syntax-Guided Synthesis Problems
• Results and Analysis of SyGuS-Comp'15
• Using SyGuS to Synthesize Reactive Motion Plans

Cited by in corpus (11)

• Programming Not Only by Example
• Just-in-Time Learning for Bottom-Up Enumerative Synthesis
• Write, Execute, Assess: Program Synthesis with a REPL
• Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants
• SyGuS Techniques in the Core of an SMT Solver
• LoopInvGen: A Loop Invariant Generator based on Precondition Inference
• Representing Partial Programs with Blended Abstract Semantics
• GXJoin: Generalized Cell Transformations for Explainable Joinability
• TabulaX: Leveraging Large Language Models for Multi-Class Table Transformations
• Type-driven Neural Programming by Example
• Proving Unrealizability for Syntax-Guided Synthesis