Efficient SMT solving for bit vectors and the extensional theory of arrays

Satisfiability Modulo Theories (SMT) solving is becoming increasingly important in academia and industry. SMT solvers are used as core decision engines for real world problems in domains such as formal verification, bug-finding, symbolic execution and test case generation. This book addresses the problem of designing, implementing, testing, and debugging an efficient SMT solver for the quantifier-free extensional theory of arrays, combined with bit-vectors. It covers correctness proofs, a complexity analysis, and implementation and optimization details such as symbolic overflow detection, propagation of unconstrained variables, and under-approximation techniques for bit-vectors. Finally, the effectiveness of black box fuzz testing and delta debugging techniques is demonstrated for SMT solver development.