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
|
| _version_ | 1797104745448472576 |
|---|---|
| author | Brain, M D'Silva, V Griggio, A Haller, L Kroening, D |
| author2 | Logozzo, F |
| author_facet | Logozzo, F Brain, M D'Silva, V Griggio, A Haller, L Kroening, D |
| author_sort | Brain, M |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T06:37:52Z |
| format | Conference item |
| id | oxford-uuid:f84711d3-41c8-4af6-84fd-19d350387146 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:37:52Z |
| publishDate | 2013 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:f84711d3-41c8-4af6-84fd-19d3503871462022-03-27T12:49:09ZInterpolation-based verification of floating-point programs with abstract CDCLConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f84711d3-41c8-4af6-84fd-19d350387146Symplectic Elements at OxfordSpringer2013Brain, MD'Silva, VGriggio, AHaller, LKroening, DLogozzo, FFähndrich, MOne 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. |
| spellingShingle | Brain, M D'Silva, V Griggio, A Haller, L Kroening, D Interpolation-based verification of floating-point programs with abstract CDCL |
| title | Interpolation-based verification of floating-point programs with abstract CDCL |
| title_full | Interpolation-based verification of floating-point programs with abstract CDCL |
| title_fullStr | Interpolation-based verification of floating-point programs with abstract CDCL |
| title_full_unstemmed | Interpolation-based verification of floating-point programs with abstract CDCL |
| title_short | Interpolation-based verification of floating-point programs with abstract CDCL |
| title_sort | interpolation based verification of floating point programs with abstract cdcl |
| work_keys_str_mv | AT brainm interpolationbasedverificationoffloatingpointprogramswithabstractcdcl AT dsilvav interpolationbasedverificationoffloatingpointprogramswithabstractcdcl AT griggioa interpolationbasedverificationoffloatingpointprogramswithabstractcdcl AT hallerl interpolationbasedverificationoffloatingpointprogramswithabstractcdcl AT kroeningd interpolationbasedverificationoffloatingpointprogramswithabstractcdcl |