Paper Info
Title
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL.
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.
Year
DOI
Venue
2013
10.1007/978-3-642-38856-9_22
Lecture Notes in Computer Science
Field
DocType
Volume
Conflict-Driven Clause Learning,Programming language,Floating point,Abstract interpretation,Computer science,Delegate,Interpolation,Theoretical computer science
Conference
7935
ISSN
Citations 
PageRank 
0302-9743
13
0.57
References 
Authors
22
5
Name
Order
Citations
PageRank
Martin Brain127922.41
Vijay D'Silva223914.07
Alberto Griggio362436.37
Leopold Haller41276.93
Daniel Kroening5432.92