SyGuS-Comp'15的结果与分析

Rajeev Alur; Dana Fisman; Rishabh Singh; Armando Solar-Lezama

doi:10.4204/EPTCS.202.3

SyGuS-Comp'15的结果与分析

编程语言 2016-02-04 v1 软件工程

作者: Rajeev Alur , Dana Fisman , Rishabh Singh , Armando Solar-Lezama

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

语法引导合成(SyGuS)是一个计算问题，即寻找一个实现f，使其同时满足由背景理论T中的逻辑公式 $\varphi$ 给出的语义约束，以及由语法G给出的句法约束，其中G规定了允许的候选实现集合。此类合成问题可以在SyGuS-IF中形式化定义，该语言构建于SMT-LIB之上。语法引导合成竞赛(SyGuS-comp)旨在通过提供一个在综合基准集上评估不同合成技术的平台，来促进、汇聚并加速针对SyGuS的高效求解器的研发。在今年的竞赛中，我们增加了两个专门赛道：一个用于条件线性算术的赛道，其中语法无需指定，并隐式假定为SMT-LIB的LIA逻辑所对应的语法；以及一个用于不变式合成问题的赛道，带有符合不变式合成问题结构的特殊构造。本文展示并分析了SyGuS-comp'15的结果。

关键词

语法引导合成 sygus-comp 程序合成 smt-lib 不变式合成条件线性算术基准评估

引用

@article{arxiv.1602.01170,
  title  = {Results and Analysis of SyGuS-Comp'15},
  author = {Rajeev Alur and Dana Fisman and Rishabh Singh and Armando Solar-Lezama},
  journal= {arXiv preprint arXiv:1602.01170},
  year   = {2016}
}

备注

In Proceedings SYNT 2015, arXiv:1602.00786

SyGuS-Comp'15的结果与分析

摘要

关键词

引用

备注

相关论文