Results and Analysis of SyGuS-Comp'15
Results and Analysis of SyGuS-Comp'15
复制标题
SyGuS-Comp15 的结果和分析
DOI：
10.4204/eptcs.202.3
复制
发表时间：
2016
影响因子：
1.6
通讯作者：
Armando Solar
中科院分区：
文献类型：
--
作者：
R. Alur;D. Fisman;Rishabh Singh;Armando Solar
语法引导合成（Syntax-Guided Synthesis，SyGuS）是一个计算问题，即寻找一个实现f，它既满足背景理论T中的逻辑公式$\varphi $给出的语义约束，又满足语法G给出的语法约束，语法G指定了允许的候选实现集。这样的合成问题可以在SyGuS-IF中正式定义，SyGuS-IF是一种建立在SMT-LIB之上的语言。
Syntax-Guided Synthesis Competition（SyGuS-comp）旨在通过提供一个平台，在一套全面的基准上评估不同的合成技术，从而促进、汇集和加速SyGuS高效求解器的研究和开发。在今年的比赛中，我们增加了两个专门的轨道：一个轨道的条件线性算术，其中的语法不需要指定，并隐含地假设是SMT-LIB的LIA逻辑，和一个轨道不变的合成问题，与特殊的结构符合不变的合成问题。本文介绍并分析了SyGuS-comp '15的结果。
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 two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. This paper presents and analyzes the results of SyGuS-comp'15.