The FixIt Model Checking Tool
The introduction of symbolic model checking, coupled with BDDs as an underlying representation, has led to significant progress in the size and diversity of systems susceptible of being automatically verified. However crucial the role of BDDs has been in that achievement, they also have known drawbacks. Examples of such drawbacks include the need of manually fed variable ordering, or size explosion for well-known classes of problems.
In this work, we replace BDDs by a non-canonical data- structure, coupled with a SAT-procedure for efficient checking of satisfiability of propositional formulae. Based on this principle, we have implemented a tool: FixIt. This tool performs standard fixed-point reachability analysis.
We present the algorithm and the main implementation issues of FixIt. We also report on current work, and show some comparative results.