FocusCheck: A tool for model checking and debugging sequential C programs 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
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009)
- Collavizza, Hélène; Rueher, Michel: Exploration of the capabilities of constraint programming for software verification (2006)
- Keller, Curtis W.; Saha, Diptikalyan; Basu, Samik; Smolka, Scott A.: FocusCheck: A tool for model checking and debugging sequential C programs (2005)