Loop Invariants on Demand

This paper describes a sound technique that combines the precision em 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 n 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.

• Type: Conference
• Year: 2005
• Where: APLAS
• Authors: K. Rustan M. Leino, Francesco Logozzo
• Keywords: APLAS 2005, Loop Invariant Arises, Loop Invariants, Loop-invariant Inference, Programming Languages