Understanding Counterexamples with explain

Autor:	Flavio Lerda, Alex Groce, Daniel Kroening
Rok vydání:	2004
Předmět:	Model checking Bounded model checker Theoretical computer science Computer science Metric (mathematics) User interface Symbolic execution Counterexample
Zdroj:	Computer Aided Verification ISBN: 9783540223429 CAV Scopus-Elsevier
DOI:	10.1007/978-3-540-27813-9_35
Popis:	The counterexamples produced by model checkers are often lengthy and difficult to understand. In practical verification, showing the existence of a (potential) bug is not enough: the error must be understood, determined to not be a result of faulty specification or assumptions, and, finally, located and corrected. The explain tool uses distance metrics on program executions to provide automated assistance in understanding and localizing errors in ANSI-C programs. explain is integrated with CBMC, a bounded model checker for the C language, and features a GUI front-end that presents error explanations to the user.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c9ebdb421a2b447886afa86efb75f35c https://doi.org/10.1007/978-3-540-27813-9_35 Zobrazit plný text záznamu