Solving difficult SMT instances using abstractions and incremental SMT solving

The satisfiability modulo theory (SMT) problem deals with deciding numerous fragments of the first-order logic constraint by some Theory $T$ and can be considered an extension of the satisfiability problem for propositional logic formulae. A SMT-Theory $T$ usually constraints the behaviour of certain uninterpreted functions or predicates of the first-order logic, but it may also syntactically constrain the language (e.g. by not allowing quantifiers). Today, solving SMT problems has become a discipline of its own with many solving techniques relying in one way or another on a SAT solver in the background. With SMT-LIB a unified interface to codify SMT instances has been developed that is supported by most state-of-the-art SMT solvers.

Over the last decade a variety of approximation techniques have been introduced into the world of SMT solving and model checking. The objective of any such approximation techniques is to speed up the solving process thus reducing computational cost and avoiding exponential runtimes for common usecases. Usually, over-approximation techniques help in speeding up the solver’s runtime for unsatisfiable SMT-instances, while under-approximation techniques help reducing the runtime of satisfiable instances.

Although abstraction techniques have successfully been used for the array theory as well as the uninterpreted functions theory, there is little work on using over-approximations for the quantifier free bitvector logic (QF_BV in SMT-LIB) outside the approach taken with UCLID. In my bachelor thesis I therefore took up the topic of solving difficult bitvector SMT instances, like the ones provided in the LLBMC family of benchmarks, using abstractions.