SyGuS-Comp 2016: Results and Analysis

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

SyGuS-Comp 2016: Results and Analysis

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1611.07627 v1 pith:CRWYE2TP submitted 2016-11-23 cs.SE cs.LGcs.LO

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

classification cs.SEcs.LGcs.LO

keywords synthesissygus-comptheorycompetitionconstraintgivenproblemresults

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

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

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

GXJoin: Generalized Cell Transformations for Explainable Joinability
cs.DB 2025-05 conditional novelty 6.0 of 10

Adding relative indexes, reusable and optional rule parts, bidirectional search, and simplicity tie-breaking raises the coverage of the best discovered transformation by up to about 10% on the authors' benchmarks.

Pith tools