SMT - Bit Vectors

My Master seminar paper about SMT solving in the theory of bit vectors is now available under Publications.


Due to how real computers are designed, SMT formulas built on unbounded integers aregenerally unsuited for deciding properties on program code and instead, sequences of bits,calledbit vectors, are used to represent machine integers. After establishing a calculus forSMT formulas on such data, this document elaborates on how these can be automaticallydecided by using theflatteningapproach to translate them into propositional logic, which canbe solved by any SAT solver. This approach is extended toincremental flattening, which isable to decide certain types of formulas significantly faster. For these processes, an exemplarilyimplementation in Haskell is developed, which is finally being used to solve a small CrackMe-challenge as an example application.