Spatial interpolants

DOI10.1007/978-3-662-46669-8_26MaRDI QIDQ2802459zbMATH OpenOpenAlexFDO

Authors Aws Albargouthi, Josh Berdine, Byron Cook, Zachary Kincaid

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.04100

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Abstract: 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.

Recommendations

• Complete instantiation-based interpolation
• Complete instantiation-based interpolation
• Effectively propositional interpolants
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Constraint Solving for Interpolation

Cited in

(6)

• A learning-based approach to synthesizing invariants for incomplete verification engines
• Spatial interpolation of high-frequency monitoring data
• Counterexample validation and interpolation-based refinement for forest automata
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• scientific article; zbMATH DE number 6126667 (Why is no real title available?)
• Space-time interpolants

This page was built for publication: Spatial interpolants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802459)