Download PDFOpen PDF in browser

Loopfrog — loop summarization for static analysis

2 pagesPublished: June 22, 2012

Abstract

Loopfrog is a scalable static analyzer for ANSI-C programs, that combines the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it does not calculate the abstract fix-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (e.g., loops) using a loop summarization algorithm. Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the sum- marization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation. It also provides “leaping” counterexamples to aid in the diagnosis of errors.

Keyphrases: loop summarization, static analysis, loopfrog, loop invariants

In: Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner (editors). WING 2010. Workshop on Invariant Generation 2010. EPiC Series in Computing, vol 1, pages 130-131

Download PDFOpen PDF in browser