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 verication such as test pattern generation, equivalence checking, assertion based verication 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 ecient decision procedure for Satisability Modulo the Theory of xed-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 a