CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishPractical 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. 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Loopfrog: A Static Analyzer for ANSI-C Programs |
| Autori: | |
| Data di pubblicazione: | 2009 |
| Abstract: | 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. 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. |
| Handle: | http://hdl.handle.net/11582/5004 |
| ISBN: | 9780769538914 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11582/5004
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Copyright © 2020