Sciweavers

KBSE
2009
IEEE

Loopfrog: A Static Analyzer for ANSI-C Programs

14 years 7 months ago
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.
Daniel Kroening, Natasha Sharygina, Stefano Tonett
Added 21 May 2010
Updated 21 May 2010
Type Conference
Year 2009
Where KBSE
Authors Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger
Comments (0)