EasyChair Publications
Search
Paper Information
Paper:Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger
Loopfrog — loop summarization for static analysis
Title:Loopfrog — loop summarization for static analysis
Authors:Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger
Keyphrases:loop summarization, static analysis, loopfrog, loop invariants
Paper:
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.
Volume:Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner (editors). WING 2010. Workshop on Invariant Generation 2010
Series:EPiC Series in Computing
Volume number:1
Pages:130-131
Editors:Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner
Page views:15
Downloads:14
BibTeX entry:
@inproceedings{WING2010:Loopfrog_loop_summarization_for_static_analysis,
  author    = {Daniel Kroening and Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich and Christoph M. Wintersteiger},
  title     = {Loopfrog -- loop summarization for static analysis},
  booktitle = {WING 2010. Workshop on Invariant Generation 2010},
  editor    = {Andrei Voronkov and Laura Kovacs and Nikolaj Bjorner},
  series    = {EPiC Series in Computing},
  volume    = {1},
  pages     = {130-131},
  year      = {2012},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}