Abstract
Bit-precise reasoning in the context of Satisfiability Modulo Theories (SMT) is a key requirement for many formal methods applications, both in industry and academia. Efficiently reasoning about bit-vector constraints in SMT has been an ongoing challenge for many years. Existing approaches all struggle with scalability for increasing bit widths, especially in the presence of arithmetic operators. The dominant state-of-the-art approach for bit-vector reasoning is bit-blasting, an eager reduction to propositional logic, which is combined with aggressive simplifications of the input constraints prior to the actual reduction step. And even though bit-blasting may come at the cost of significantly increasing the formula size, which is the main reason for scalability issues with this technique, it is surprisingly efficient in practice---thanks to state-of-the-art SAT solvers. This talk will explore the main challenges for bit-vector reasoning and highlight state-of-the-art techniques. In particular, we will present a recent procedure that aims at improving the scalability of bit-blasting.