This paper describes a sound technique that combines the precision of theorem proving with the loop-invariant inference of abstract interpretation. The loop-invariant computations are invoked on demand when the need for a stronger loop invariant arises, which allows a gradual increase in the level of precision used by the abstract interpreter. The technique generates loop invariants that are specific to a subset of a program's executions, achieving a dynamic and automatic form of value-based trace partitioning. Finally, the technique can be incorporated into a lemmas-on-demand theorem prover, where the loop-invariant inference happens after the generation of verification conditions. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Leino, K. R. M., & Logozzo, F. (2005). Loop invariants on demand. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3780 LNCS, pp. 119–134). https://doi.org/10.1007/11575467_9
Mendeley helps you to discover research relevant for your work.