@conference {153,
	title = {Loopfrog: A Static Analyzer for ANSI-C Programs},
	booktitle = {The 24th IEEE/ACM International Conference on Automated Software Engineering},
	year = {2009},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Auckland, New Zealand},
	abstract = {
<p style="margin-top: 0px; margin-bottom: 1.5em; color: rgb(73, 73, 73); font-family: {\textquoteright}Lucida Grande{\textquoteright}, {\textquoteright}Bitstream Vera Sans{\textquoteright}, Arial, sans-serif;  text-align: justify;">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 explosion problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives.</p>
<p style="margin-top: 0px; margin-bottom: 1.5em; color: rgb(73, 73, 73); font-family: {\textquoteright}Lucida Grande{\textquoteright}, {\textquoteright}Bitstream Vera Sans{\textquoteright}, Arial, sans-serif;  text-align: justify;">We present Loopfrog, a static analyzer that combines the best of both worlds: the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides "leaping" counterexamples to aid in the diagnosis of errors.</p>
},
	author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.}
}
