SyGuS-Comp 2017: Results and Analysis
Rajeev Alur University of PennsylvaniaBen-Gurion UniversityMicrosoft Research, RedmondMassachusetts Institute of Technology Dana Fisman Ben-Gurion UniversityMicrosoft Research, RedmondMassachusetts Institute of Technology Rishabh Singh Microsoft Research, RedmondMassachusetts Institute of Technology Armando Solar-Lezama Massachusetts Institute of Technology
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.
中文速览
语法制导综合（Syntax-Guided Synthesis，SyGuS）要解决的是：给定一个逻辑规范和一套语法约束，自动找出满足二者的程序实现。2017年第四届SyGuS竞赛共有六支求解器参赛，在超过1500个测试基准上展开角逐，涵盖通用、条件线性整数算术、循环不变式生成以及编程示例四个赛道。结果显示，EUSolver_2017在综合基准数量上领先，CVC4_2017和Euphony紧随其后，而专项求解器LoopInvGen和e3solver则分别在不变式生成和位向量编程示例赛道上表现突出。这项竞赛为程序合成领域提供了客观的横向比较平台，推动了各类合成技术（枚举、反例引导、统计语言模型等）的持续进步，也揭示了指令选择等方向上仍存在所有求解器均无法攻克的难题。
原文 arXiv:1711.11438;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1711.11438v1