A Complete Approach to Loop Verification with Invariants and Summaries

Loop invariants characterize the partial result computed by a loop so far up to an intermediate state. Such invariants are correct, if they can be propagated forward through arbitrary iterations. Invariants can be complemented by summaries that characterize the remaining iterations as a binary relation between intermediate states to possible final states. Dually to invariants, summaries are correct if the intermediate state of reference can be propagated backwards towards the starting state, which may often encode the bulk of the correctness of a loop more naturally. In this paper, we derive sound verification conditions for this approach, and moreover characterize completeness relative to a class of "safe" invariants, alongside with fundamental and novel insights in the relation between invariants and summaries. All theoretical results have immediate practical consequences for tool use and construction. A preliminary evaluation of automation potential shows that the proposed approach is competitive, even without specialized solving strategies.