Getafix ("get-a-fix using fixpoints")
is a symbolic model checker for Boolen programs (currently
supporting reachability only). It translates sequential and concurrent Boolean programs into
Boolean formulae, and using a fixed-point solver (the model-checker
Mucke), solves the reachability
problem symbolically using Boolean Decision Diagrams (BDDs).
A salient aspect
of the tool is that the entire reachability algorithm is written
using a simple mu-calculus formula, spanning just a few lines!
Getafix implements a reachability algorithm for sequential programs that computes summaries by pushing
entries forward (see below for the templates for the algorithms).
Getafix also implements k-bounded context-switching reachability, which is written,
again, using a fixed-point formula.
Experimental results show that Getafix is competitive with existing mature
solvers (BEBOP and Moped)
(see below).
BEBOP is the the model-checker that ships with
Microsoft's Static Driver Verifier toolkit).
More details on Getafix can be found in this paper:
Analyzing Recursive Programs using a Fixed-point Calculus
by S. La Torre, P. Madhusudan, and G. Parlato.
ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI),
Dublin, Ireland, 2009.
Getafix for sequential Boolean programs
- Model-checking algorithms written as simple formulas:
The reachability algorithm for sequential recursive programs is expressed as a simple fixed-point formula:
There are two versions:
- Entry-forward (EF) that computes summaries by pushing the entry forward;
Click here for the formula
- An optimized entry-forward algorithm that computes images only on states with a program counter that changed in the last round
Click here for the formula
- Download
Download the Getafix tool. Click here to download the source code that converts Boolean programs to Mucke code.
This does do some variable elimination (dead variables are removed,
etc.), code simplification, and determines a BDD variable order.
The templates above then implement the model-checker for the program.
- Experiments
Click here for experiments on sequential program benchmarks, and
comparisons with Bebop and Moped.
Getafix for concurrent Boolean programs:
Getafix implements reachability within a fixed number of context-switches for concurrent recursive Boolean programs.
Model-checking algorithm as formulas:
Reachability in concurrent programs within k context-switches is expressed as a fixed-point formula.
Here is a sample reachability formula for two threads and four context-switches: 4CStemplate.
Experiments:
Click here for experiments on a model
of a Windows NT Bluetooth driver
Getafix can convert concurrent programs to sequential programs:
A component of Getafix can also effect a translation from concurrent Boolean
programs to sequential Boolean programs, which reduces reachability within
a bounded number of context-switches in the concurrent program to reachability
in the sequential program. The salient feature is that the sequential
program will track, at any point, the shared variables and the local variables
of only
one process.
Click here to see the conversion tool and the associated paper in CAV'09
Contact
Getafix has been devoloped by Salvatore La Torre, P. Madhusudan, and Gennaro Parlato.
This material is based upon work supported by the National Science Foundation under Grant No. #0747041. Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).
