A Lightweight Approach for Loop Summarization

A problem common to most of the tools based on the abstraction refinement paradigm is the divergence of the CEGAR process. In particular, infinitely many (spurious) counterexamples may arise from unfolding the same (

while

- or

for

-) loop in the given program again and again; this leads to an infinite or at least too large sequence of refinement steps. Loop summarization is an approach that permits to overcome this problem. It consists of abstracting not just states but also the state changes (transition relation) induced by structured program statements. The effectiveness of this approach depends on two factors: (

a

) the computation of loop summaries must not be the bottleneck of the verification algorithm (

b

) loop summaries must be precise enough to prove the property of interest. We present a technique that permits to achieve both goals. It uses inference rules to compute summaries. A lightweight test is performed to check whether a given loop matches the premise of a given rule. If so, a summary is automatically inferred by instantiating the rule. Despite its simplicity, our technique performs well in practice. We were able to verify safety properties for many examples which are out of the scope of several existing tools.