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

  • Curtis W. Keller
  • Diptikalyan Saha
  • Samik Basu
  • Scott A. Smolka
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


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.


  1. 1.
    Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Basu, S., Saha, D., Lin, Y.-J., Smolka, S.A.: Generation of all counter-examples for push-down systems. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Basu, S., Saha, D., Smolka, S.A.: Counter-example analysis for Cimple debugging. In: Proceedings of FORTE (2004)Google Scholar
  4. 4.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL (2002)Google Scholar
  5. 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. 6.
    RTCA. Minimum operational performance standards for traffic alert and collision avoidance system (TCAS) airborne equipment consolidated edition (1990)Google Scholar
  7. 7.
    Saidi, H.: Model checking guided predicate abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    XSB. The XSB logic programming system,

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Curtis W. Keller
    • 1
  • Diptikalyan Saha
    • 2
  • Samik Basu
    • 1
  • Scott A. Smolka
    • 2
  1. 1.Department of Computer ScienceIowa State UniversityAmes
  2. 2.Department of Computer ScienceState University of New YorkStony Brook

Personalised recommendations