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

    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

    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).