Loopfrog: A Static Analyzer for ANSI-C Programs

—Practical software verification is dominated by two major classes of techniques. The first is model checking, which provides total precision, but suffers from the state space n problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives. We present LOOPFROG, a static analyzer that combines the best of both worlds: the precision of ecking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides ‘leaping’ counterexamples to aid in the diagnosis of errors.

• Type: Conference
• Year: 2009
• Where: KBSE
• Authors: Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
• Keywords: Abstract Interpretation, KBSE 2009, Software Engineering, Static Analyzers, —Practical Software Verification