Recursive Games for Compositional Program Synthesis
Recursive Games for Compositional Program Synthesis
复制标题
用于组合程序综合的递归博弈
DOI：
10.1007/978-3-319-29613-5_2
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Rybalchenko
中科院分区：
文献类型：
--
作者：
Beyene;Chaudhuri;Popeea;Rybalchenko
组合性，即使用过程摘要而不是代码内联，是将自动验证扩展到大型代码库的关键。在本文中，我们提出了一种在程序综合的背景下利用组合性的方法。我们综合问题的目标是实例化过程程序中缺失的表达式，以便生成的程序在对抗性环境下满足安全或终止要求。该问题被建模为两个玩家（程序和环境）之间的游戏，这两个玩家轮流改变程序的状态和堆栈。该程序的目标是确保该递归游戏的所有执行都满足要求。综合涉及程序满足此目标的策略的模块化计算。我们的解决方案基于游戏摘要的概念，它概括了传统的过程摘要，并将过程上下文中的程序状态与游戏可以从该上下文返回的状态集相关联。我们关于游戏摘要的组合推理方法体现在一组演绎证明规则中。我们证明这些规则是合理且相对完整的。我们还表明，可以使用 Horn 约束求解器来自动化这些规则的合理近似，该求解器利用 SMT 求解、反例引导的抽象细化和插值。对一组系统代码基准的实验评估证明了该方法的实际前景。
Compositionality, i.e., the use of procedure summarization instead of code inlining, is key to scaling automated verification to large code bases. In this paper, we present a way to exploit compositionality in the context ofprogram synthesis.The goal in our synthesis problem is to instantiate missing expressions in a procedural program so that the resulting program satisfies a safety or termination requirement in spite of an adversarial environment. The problem is modeled as a game between two players — the program and the environment — that take turns changing the program’s state and stack. The objective of the program is to ensure that all executions of thisrecursive gamesatisfy the requirement. Synthesis involves the modular computation of a strategy under which the program meets this objective. Our solution is based on the notion ofgame summaries, which generalize traditional procedure summaries, and relate program states in a procedural context with sets of states at which the game can return from that context. Our method for compositional reasoning about game summaries is embodied in a set of deductive proof rules. We prove these rules sound and relatively complete. We also show that a sound approximation of these rules can be automated using a Horn constraint solver that utilizes SMT-solving, counterexample-guided abstraction refinement, and interpolation. An experimental evaluation over a set of systems code benchmarks demonstrates the practical promise of the approach.
登录
查看更多内容
综合反应式程序
DOI：
10.4230/lipics.csl.2011.428
发表时间：
2011
期刊：
2006 Formal Methods in Computer Aided Design
影响因子：
--
作者：
P. Madhusudan
通讯作者：
P. Madhusudan
应用 C 语言修复布尔程序
DOI：
10.1007/11817963_33
发表时间：
2006
期刊：
Proceedings of the XXXV Brazilian Symposium on Software Engineering
影响因子：
--
作者：
Andreas Griesmayer;R. Bloem;B. Cook
通讯作者：
B. Cook
嵌套树的语言
DOI：
--
发表时间：
2006
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
R. Alur;Swarat Chaudhuri;P. Madhusudan
通讯作者：
P. Madhusudan
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
发表时间：
2013
期刊：
影响因子：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko
局部和全局程序流的不动点演算
DOI：
--
发表时间：
2006
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
R. Alur;Swarat Chaudhuri;P. Madhusudan
通讯作者：
P. Madhusudan