Bit-level Analysis Tool, version 0.2

Welcome to the homepage of BAT, the Bit-level Analysis Tool. BAT implements a state-of-the-art decision procedure for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories). Such problems often appear in hardware, software, and security domains. BAT uses innovative techniques for efficiently translating from the high-level BAT language into tractable SAT problems. These techniques include:

Key features of the BAT language are:

The result is a tool that can solve problems that cannot be handled by any other decision procedure we have tried. For example, BAT can prove that a 32-bit 5 stage pipelined machine model refines its ISA in approximately 2 minutes. We know of no other tools that can solve even much simpler pipeline machine examples. See the benchmarks page for this and other benchmarks.

To find out more about BAT or to use it yourself, see the links along the left side of this website.

Contact us if you have any questions or want to collaborate on interesting applications.

The authors are Pete Manolios (Advisor), Sudarshan Srinivasan (Applications and Benchmarks), and Daron Vroon (Developer).