Sciweavers

Share
POPL
2003
ACM

From symptom to cause: localizing errors in counterexample traces

10 years 1 months ago
From symptom to cause: localizing errors in counterexample traces
There is significant room for improving users' experiences with model checking tools. An error trace produced by a model checker can be lengthy and is indicative of a symptom of an error. As a result, users can spend considerable time examining an error trace in order to understand the cause of the error. Moreover, even state-of-the-art model checkers provide an experience akin to that provided by parsers before syntactic error recovery was invented: they report a single error trace per run. The user has to fix the error and run the model checker again to find more error traces. We present an algorithm that exploits the existence of correct traces in order to localize the error cause in an error trace, report a single error trace per error cause, and generate multiple error traces having independent causes. We have implemented this algorithm in the context of Slam, a software model checker that automatically verifies temporal safety properties of C programs, and report on our exp...
Thomas Ball, Mayur Naik, Sriram K. Rajamani
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where POPL
Authors Thomas Ball, Mayur Naik, Sriram K. Rajamani
Comments (0)
books