General Description

FocusCheck is a model checker for sequential C programs and assertion properties. It follows the typical abstraction-refinement technique: infinite domain variables are abstracted while identifying violating paths (counter-examples) and constraint solver is used to discard all infeasible counter-examples. Three important distinguishing features of FocusCheck are:

• all (finite number) feasible counter-examples which are loop-free and require minimum number of recursion are generated.
• counter-example is sliced to identify a subsequence, Focus Statement Sequence, which directly or indirectly causes the error underlying the counter-example. Feasibility of FSS implies the existence of feasible counter-example. Furthermore, constraints, assumptions, on input/uninitialized variables can be identified that are required for the feasibility.
• FocusCheck analyzes the FSSs and the corresponding assumptions and can zoom in on specific program segments, Neighborhood of Error Statements, that are most likely to harbor the error statements in the program, thereby helping in easy debugging and readability of model checking results.
FocusCheck is equipped with a simple and intuitive Graphical User Interface which presents the user various different views of the counter-examples and the associated information.

Getting Started

If you would like to see how FocusCheck works before installing see the Documentation or click here

The core of FocusCheck is written XSB logic programming engine. It uses a number of packages for translating C source-code to XSB readable format. To install and use FocusCheck in Linux follow the steps below(each package has its own installation instruction):

• Download ocaml
• Download CIL (you can also use pre-compiled libraries)
• Download c2ast (To configure, update the path to the cil libraries in the configure file. Make sure c2ast is present in your path or you can give the path of c2ast to the model checker, see below).
• Download XSB (tar) or get XSB2.6 from sourceforge (make sure xsb is present in your path)
• Download FocusCheck (If xsb is not present in your path, modify the verify and post scripts at the top-directory and provide the location of xsb executable. Replace "xsb" in the scripts with "myxsbpath/bin/xsb". Similarly, if c2ast is not present in your path, modify the verify script).


Documentation

Members

Curtis W. Keller, Samik Basu: Iowa State University
Diptikalyan Saha, Scott A. Smolka: State University of New York at Stony Brook

Publications

• Samik Basu, Diptikalyan Saha and Scott A. Smolka
  Localizing Program Errors for Cimple Debugging
  International Conference on Formal Techniques for Networked and Distributed Systems 2004
• Samik Basu, Diptikalyan Saha, Yow-Jian Lin and Scott A. Smolka
  Generation of All Counter-Examples for Push-Down Systems
  International Conference on Formal Techniques for Networked and Distributed Systems 2003
• Samik Basu, K. Narayan Kumar, Robert L. Pokorny and C.R. Ramakrishan
  Resource Constrained Model Checking for Push-down Systems
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2002