Deciding floating-point logic with systematic abstraction

Abstract

Bit-precise decision procedures for reasoning about machine data types are of fundamental importance for software verification. We present a bit-precise decision procedure for the theory of binary floating-point arithmetic. Current solvers for this theory are based on bit-vector encodings. Propositional solvers based on the Conflict Driven Clause Learning (CDCL) algorithm are used as a back-end. We present a natural-domain SMT approach that lifts the CDCL framework to operate directly over abstractions of floating-point assignments. The core of our approach is a non-trivial generalisation of the conflict analysis algorithm used in modern SAT solvers. We have instantiated our method inside MATHSAT5 with the floating-point interval abstraction. The result is a sound and complete procedure for floating-point arithmetic that outperforms the state-of-the- art significantly on problems that check ranges on numerical variables. Our technique is independent of the specific abstraction used and can modularly be extended to provide natural-domain reasoning for other applications.