# SyGuS-Comp 2016: Results and Analysis

arXiv: https://arxiv.org/abs/1611.07627 · HTML: https://mlsanity.com/paper/1611.07627/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Nov 2016.

## Built on by (most cited first, 2 of 2)

- [Program Synthesis with Best-First Bottom-Up Search](https://mlsanity.com/paper/2310.04327/) (2023)
- [TabulaX: Leveraging Large Language Models for Multi-Class Table Transformations](https://mlsanity.com/paper/2411.17110/) (2024)

## Abstract (arXiv)

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 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.