Name
Abstract | ||
|---|---|---|
We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been extensively studied from a theoretical viewpoint as a classical means of program verification, in practice existing tools do not scale even to moderately sized programs. This is because the constraints that need to be solved even for small programs are already too difficult for the underlying (non-linear) constraint solving engines. To overcome this obstacle, we propose to strengthen static constraint generation with information obtained from static abstract interpretation and dynamic execution of the program. The strengthening comes in the form of additional linear constraints that trigger a series of sim- plifications in the solver, and make solving more scalable. We demonstrate the practical applicability of the approach by an experimental evaluation on a col- lection of challenging benchmark programs and comparisons with related tools based on abstract interpretation and software model checking. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/s10009-012-0267-5 | Tools and Algorithms for Construction and Analysis of Systems |
Keywords | DocType | Volume |
Invariant generation, Linear invariants, Constraint solving, Testing, Software verification | Journal | 15 |
Issue | ISSN | Citations |
4 | 1433-2787 | 25 |
PageRank | References | Authors |
1.17 | 18 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ashutosh Gupta | 1 | 192 | 14.01 |
| Rupak Majumdar | 2 | 3401 | 220.08 |
| Andrey Rybalchenko | 3 | 1439 | 68.53 |