Reasoning about Data: Bits, bit vectors, or words

Summary form only given. Many techniques for test generation and verification require reasoning about data using automated mathematical or logical techniques. Classical methods for specifying and reasoning about programs consider each word to be an arbitrary numeric value. This has carried over into many program analysis tools, where decision procedures for integer or real arithmetic are used to reason about program behavior. At the other extreme, most automatic methods for reasoning about hardware operate at the bit level, viewing each signal as an independent Boolean function of the input and state bits. In between these extremes, data can be modeled by finite-precision arithmetic and bit-wise operations on fixed-width data words. A decision procedure for such a bit-vector model can accurately capture the behavior of actual systems, while also exploiting abstraction techniques that are difficult to recognize when the system is modeled purely at the bit level. Until recently, the best way to reason about bit vectors was to simply expand formulas into their bit-level representations and apply Boolean satisfiability (SAT) solvers. Several newer decision procedures have improved on this approach by combining SAT solving with word-level abstractions. Work in this area is already having major impact in both program analysis and hardware testing and verification.