Loopfrog — loop summarization for static analysis

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 tran... View More