Abstract
One approach for smt solvers to improve efficiency is to delegate reasoning to abstract domains. Solvers using abstract domains do not support interpolation and cannot be used for interpolation-based verification. 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. © 2013 Springer-Verlag.
Cite
CITATION STYLE
Brain, M., D’Silva, V., Griggio, A., Haller, L., & Kroening, D. (2013). Interpolation-based verification of floating-point programs with abstract CDCL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7935 LNCS, pp. 412–432). https://doi.org/10.1007/978-3-642-38856-9_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
