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
|