The analysis engine is fairly mature at this point: it comprises roughly 70,000 lines of C++ and C code, as well as standard C++ templates, yacc generation code, etc.
We are currently investigating model-checking on infinite-state programs [ CAV97]. In infinite transition systems, the problem gets substantially harder -- and many basic properties are undecidable. Hence we are attacking the problem using conservative techniques, in concert with a symbolic model checker, which uses Presburger formulas to encode a program's transition system (as well as its model-checking computations). Fixpoint calculations are executed symbolically, and their convergence is guaranteed by using several approximation techniques. This method has yielded some very promising results; to date, it was successfully verified safety and liveness properties on several infinite-state systems, commonly used in standard concurrency applications.
However, we also discovered that our pure Presburger approach was inefficient in its treatment of Boolean and (unordered) enumerated types -- which possess no natural mapping to the Euclidean coordinate space.
To correct this problem, we developed a new set of verification techniques, which combine the strengths of both approaches. Specifically, this resulted in a composite model-checker, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. To date, we have demonstrated our technique's effectiveness on some nontrivial requirements specifications, which include mixtures Booleans, integers and enumerated types [Composite97].