Calysto (2006—2008) — Scalable Software Static Checking

Fast static checker for checking large bodies of code. Exploits the structure at several levels of granularity, which significantly improves the scalability. Based on a novel symbolic execution algorithm and structural abstraction. Tight integration with the Spear theorem prover makes it exceptionally fast.

Spear (2006—2008) — Fast Bit-vector Arithmetic Theorem Prover and SAT Solver

Fast bit-vector arithmetic (a.k.a. modular arithmetic, machine arithmetic) theorem prover and SAT solver. Supports all standard modular arithmetic operators, including signed/unsigned division and remainder. Supports several standard formats. Can be easily automatically optimized to a specific set of instances.

HyperSAT (2004—2005) — Experimental Boolean Satisfiability Solver

Experimental B-cubing based solver. B-cubes are novel data structures for search space pruning.