Interpolation-based verification of floating-point programs with abstract CDCL
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 generati...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2013
|
| Summary: | 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. |
|---|