Access Restriction

Author Rajamani, Sriram K. ♦ Naik, Mayur ♦ Ball, Thomas
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Debugging ♦ Software model checking
Abstract 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 experience using it to find and localize errors in device drivers. The algorithm typically narrows the location of a cause down to a few lines, even in traces consisting of hundreds of statements.
Description Affiliation: Microsoft Research (Ball, Thomas; Rajamani, Sriram K.) || Purdue University (Naik, Mayur)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 38
Issue Number 1
Page Count 9
Starting Page 97
Ending Page 105

Open content in new tab

   Open content in new tab
Source: ACM Digital Library