Master thesis

Bit-vector solvers typically rely on two things: powerful pre-processing of bit-vector terms and efficient SAT solver to solve the bit-blasted problem, i.e., the transformed input formula. The goal of this thesis is to review the state-of-the-art approaches to bit-vector solving and implement the most promising one in the OpenSMT solver [1]. For an approach using bit-blasting, a different heuristic for tuning the underlying SAT solver should be compared.

  1. OpenSMT:
  2. SMT-LIB:
  3. SMT-COMP: