Bit-vector solver for OpenSMT

Target

Master thesis

Contact

• Martin Blicha
• Jan Kofroň

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: https://github.com/usi-verification-and-security/opensmt/
2. SMT-LIB: http://smtlib.cs.uiowa.edu
3. SMT-COMP: https://smt-comp.github.io/2019/