Title: Towards Verifying Nonlinear Integer Arithmetic
Advisor: Paul Beame
Supervisory Committee: Paul Beame (Chair), Matthew Lorig (GSR, AMATH), Anup Rao, Dan Suciu, and Emina Torlak
Abstract: The last two decades are marked by significant advances in the power of general-purpose automated reasoning tools. Satisfiability (SAT) solvers and satisfiability modulo theories (SMT) solvers have now become standard tools, finding applications in a diverse array of problems arising from industry and academia.
The theory of fixed size bit-vectors plays a particularly important role in the context of hardware and software verification. SMT solvers for the theory of bit-vectors have advanced significantly and are considered efficient for most problems. However, bit-vector formulas involving the detailed, bit-level properties of multiplication still pose a challenge for modern solvers. The time to solve problems as basic as verifying the equivalence of two multiplication algorithms scales exponentially in the bit-width for all current SAT solvers. Yet, our recent work showed that with perfect heuristics, SAT solvers could achieve polynomial scaling.
In this talk, we will discuss the current research towards finding efficient ways to verify multiplier circuits, and towards the more general problem of deciding bit-vector formulas containing multiplication. We assess the strengths and weaknesses of various approaches towards multiplier verification and propose several future research directions based on our previous results.