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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
