FocusCheck Model Checker
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:
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.
- 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.
If you would like to see how FocusCheck works before installing see
the Documentation or click
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).
Curtis W. Keller, Samik Basu: Iowa State University
Diptikalyan Saha, Scott A. Smolka: State University of New York at Stony Brook
Last updated: 10/29/2004