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.
- 3.Basu, S., Saha, D., Smolka, S.A.: Counter-example analysis for Cimple debugging. In: Proceedings of FORTE (2004)Google Scholar
- 4.Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL (2002)Google Scholar
- 5.Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programsGoogle Scholar
- 6.RTCA. Minimum operational performance standards for traffic alert and collision avoidance system (TCAS) airborne equipment consolidated edition (1990)Google Scholar
- 8.XSB. The XSB logic programming system, http://xsb.sourceforge.net