论文标题
Synrg：语法指导与交替量词的表达式合成
SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers
论文作者
论文摘要
程序合成是自动生成满足给定规范的表达式的任务。程序合成技术已用于自动化代码中的循环不变性，合成功能摘要以及通过程序草图协助程序员。语法引导的合成在该领域已经成功范式，但是，最先进的求解器落下的领域是关于潜在无界数据结构（例如阵列）的推理，例如规格和解决方案都可能需要量词和量词交替。我们提出了Synrg，这是一种基于限制合成问题的综合算法，以生成有限域的量化解决方案，然后将这些候选溶液推广到原始规范的不受限制域。我们报告了关于不变综合基准测试和从Java Stringutils类获取的程序草图基准的实验，并表明我们的技术可以使所有现有求解器无法触及的表达式合成表达式。
Program synthesis is the task of automatically generating expressions that satisfy a given specification. Program synthesis techniques have been used to automate the generation of loop invariants in code, synthesize function summaries, and to assist programmers via program sketching. Syntax-guided synthesis has been a successful paradigm in this area, however, one area where the state-of-the-art solvers fall-down is reasoning about potentially unbounded data structures such as arrays where both specifications and solutions may require quantifiers and quantifier alternations. We present SynRG, a synthesis algorithm based on restricting the synthesis problem to generate candidate solutions with quantification over a finite domain, and then generalizing these candidate solutions to the unrestricted domain of the original specification. We report experiments on invariant synthesis benchmarks and on program sketching benchmarks taken from the Java StringUtils class and show that our technique can synthesize expressions out of reach of all existing solvers.
