Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Fate and FreeWill in Error Traces

HoonSang JinContact Information, Kavita RaviContact Information and Fabio SomenziContact Information

(6)  University of Colorado at Boulder, Boulder
(7)  Cadence Design Systems, Canada
Abstract
The ability to generate counterexamples for failing properties is often cited as one of the strengths of model checking. However, it is often difficult to interpret long error traces in which many variables appear. Further, a traditional error trace presents only one possible behavior of the system causing the failure, with no further annotation. Our objective is to “capture more of the error” in an error trace to make debugging easier.We present an enhanced error trace in an alternation of fated (forced) and free segments. The fated segments showunavoidable progress towards the error while the free segments show choices that, if avoided, may have prevented the error. This segmentation raises the questions of whether the fated segment should indeed be inevitable and whether the free segments are critical in causing the error. Addressing these questions may help the user analyze the error better.
This work was supported in part by SRC contract 2001-TJ-920 and NSF grant CCR-99-71195.

Contact Information HoonSang Jin
Email: Jinh@Colorado.EDU

Contact Information Kavita Ravi
Email: kravi@cadence.com

Contact Information Fabio Somenzi
Email: Fabio@Colorado.EDU
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb20
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)