A Lightweight Approach for Loop Summarization

Mohamed Nassim Seghir

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings
PublisherSpringer Berlin Heidelberg
Pages351-365
Number of pages15
Volume6996
ISBN (Electronic)978-3-642-24372-1
ISBN (Print)978-3-642-24371-4
DOIs
Publication statusPublished - 2011

Cite this