Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Spatial Interpolants
verfasst von : Aws Albargouthi, Josh Berdine, Byron Cook, Zachary Kincaid
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We propose
SplInter
, a new technique for proving properties of heap-manipulating programs that marries (1) a new
separation logic–based
analysis for heap reasoning with (2) an
interpolation-based
technique for refining heap-shape invariants with data invariants.
SplInter
is
property directed
,
precise
, and produces counterexample traces when a property does not hold. Using the novel notion of
spatial interpolants modulo theories
,
SplInter
can infer complex invariants over general recursive predicates, e.g., of the form
all elements in a linked list are even
or a
binary tree is sorted
. Furthermore, we treat interpolation as a black box, which gives us the freedom to encode data manipulation in any suitable theory for a given program (e.g., bit vectors, arrays, or linear arithmetic), so that our technique immediately benefits from any future advances in SMT solving and interpolation.