Sciweavers

Share
TACAS
2005
Springer

FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs

9 years 3 months ago
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs
Abstract. We present the FocusCheck model-checking tool for the verification and easy debugging of assertion violations in sequential C programs. The main functionalities of the tool are the ability to: (a) identify all minimum-recursion, loop-free counter-examples in a C program using on-the-fly abstraction techniques; (b) extract focus-statement sequences (FSSs) from counter-examples, where a focus statement is one whose execution directly or indirectly causes the violation underlying a counter-example; (c) detect and discard infeasible counter-examples via feasibility analysis of the corresponding FSSs; and (d) isolate program segments that are most likely to harbor the erroneous statements causing the counter-examples. FocusCheck is equipped with a smart graphical user interface that provides various views of counter-examples in terms of their FSSs, thereby enhancing usability and readability of model-checking results.
Curtis W. Keller, Diptikalyan Saha, Samik Basu, Sc
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TACAS
Authors Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka
Comments (0)
books