Spatial interpolants
From MaRDI portal
Publication:2802459
DOI10.1007/978-3-662-46669-8_26zbMATH Open1335.68040arXiv1501.04100OpenAlexW3037414458MaRDI QIDQ2802459FDOQ2802459
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)
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.
Full work available at URL: https://arxiv.org/abs/1501.04100
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
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
- Title not available (Why is that?)
- 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)
