Deciding Floating−Point Logic with Systematic Abstraction

Conference item

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.

Authors: Haller, L; Griggio, A; Brain, M; Kroening, D

• Host title: FMCAD
• Publication date: 2012-01-01