Interpolation-based verification of floating-point programs with abstract cdcl

Abstract. One approach for smt solvers to improve efficiency is to del-egate reasoning to abstract domains. Solvers using abstract domains do not support interpolation and cannot be used for interpolation-based ver-ification. We extend Abstract Conflict Driven Clause Learning (acdcl) solvers with proof generation and interpolation. Our results lead to the first interpolation procedure for floating-point logic and subsequently, the first interpolation-based verifiers for programs with floating-point variables. We demonstrate the potential of this approach by verifying a number of programs which are challenging for current verification tools.