Template-based program verification and program synthesis
Template-based program verification and program synthesis
复制标题
基于模板的程序验证和程序综合
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
J. Foster
中科院分区：
文献类型：
--
作者：
S. Srivastava;Sumit Gulwani;J. Foster
程序验证是自动生成程序符合给定规范的证明的任务。程序综合是自动生成满足给定规范的程序的任务。程序验证和程序综合都可以看作是搜索问题，分别用于证明和程序。对于这些搜索问题，我们提出了基于用户提供的见解的模板的形式的方法。模板是关于不变量和程序的语法形式的提示，并帮助指导搜索解决方案。我们展示了如何减少基于模板的搜索问题，满足性解决，这使得使用现成的求解器，有效地探索搜索空间。基于模板的方法使我们能够验证和合成程序的能力以外的以前的验证器和合成器。我们的方法可以验证和合成困难的算法教科书程序（例如，基于排序和动态编程的算法）和困难的算术程序。
Program verification is the task of automatically generating proofs for a program’s compliance with a given specification. Program synthesis is the task of automatically generating a program that meets a given specification. Both program verification and program synthesis can be viewed as search problems, for proofs and programs, respectively. For these search problems, we present approaches based on user-provided insights in the form of templates. Templates are hints about the syntactic forms of the invariants and programs, and help guide the search for solutions. We show how to reduce the template-based search problem to satisfiability solving, which permits the use of off-the-shelf solvers to efficiently explore the search space. Template-based approaches have allowed us to verify and synthesize programs outside the abilities of previous verifiers and synthesizers. Our approach can verify and synthesize difficult algorithmic textbook programs (e.g., sorting and dynamic programming-based algorithms) and difficult arithmetic programs.
从测试到证明
DOI：
10.1007/s10009-012-0267-5
发表时间：
2013
影响因子：
1.5
作者：
Ashutosh Gupta;Rupak Majumdar;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko