Name
Abstract | ||
|---|---|---|
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 of program 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 this recursive game satisfy the requirement. Synthesis involves the modular computation of a strategy under which the program meets this objective. Our solution is based on the notion of game 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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-29613-5_2 | VSTTE |
Field | DocType | Volume |
Principle of compositionality,Automatic summarization,Horn clause,Programming language,Expression (mathematics),Program synthesis,Computer science,Theoretical computer science,Constraint satisfaction problem,Modular design,Recursion | Conference | 9593 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.35 |
References | Authors | |
26 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tewodros A. Beyene | 1 | 70 | 3.74 |
| Swarat Chaudhuri | 2 | 981 | 67.68 |
| Corneliu Popeea | 3 | 374 | 18.27 |
| Andrey Rybalchenko | 4 | 1439 | 68.53 |