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.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka
• Keywords: Algorithms, Corresponding Fsss, Discard Infeasible Counter-examples, FocusCheck Model-checking Tool, TACAS 2005