Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT

Decision procedures for expressive logics such as linear arithmetic, bit-vectors, uninterpreted functions, arrays or combinations of theories are becoming increasingly important in various areas of hardware and software development and verification such as test pattern generation, equivalence checking, assertion based verification and model checking. In particular, the need for bit-precise reasoning is an important target for research into decision procedures. In this thesis we will describe work on creating an efficient decision procedure for Satisfiability Modulo the Theory of fixed-width bit-vectors, and how such a solver can be used in a real-world application. We will also introduce some extensions of the basic decision procedure allowing for optimisation, and compact representation of constraints in a SMT solver, showing how these can be succinctly and elegantly described as a theory allowing for the extension with minimal changes to SMT solvers.