Predicate abstraction for linked data structures

DOI10.1007/978-3-662-49122-5_3MaRDI QIDQ2796037zbMATH OpenOpenAlexFDO

Authors Alexander Bakst, Ranjit Jhala

Publication date 23 March 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We present Alias Refinement Types (ART), a new approach to the verification of correctness properties of linked data structures. While there are many techniques for checking that a heap-manipulating program adheres to its specification, they often require that the programmer annotate the behavior of each procedure, for example, in the form of loop invariants and pre- and post-conditions. Predicate abstraction would be an attractive abstract domain for performing invariant inference, existing techniques are not able to reason about the heap with enough precision to verify functional properties of data structure manipulating programs. In this paper, we propose a technique that lifts predicate abstraction to the heap by factoring the analysis of data structures into two orthogonal components: (1) Alias Types, which reason about the physical shape of heap structures, and (2) Refinement Types, which use simple predicates from an SMT decidable theory to capture the logical or semantic properties of the structures. We prove ART sound by translating types into separation logic assertions, thus translating typing derivations in ART into separation logic proofs. We evaluate ART by implementing a tool that performs type inference for an imperative language, and empirically show, using a suite of data-structure benchmarks, that ART requires only 21% of the annotations needed by other state-of-the-art verification techniques.

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Predicate abstraction for software verification
• Predicate abstraction for program verification
• Verifying properties of well-founded linked lists
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• Data abstraction: a general framework to handle program verification of data structures
• Verification of multi-linked heaps
• PDL for structured data: a graph-calculus approach
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Predicate abstraction with indexed predicates
• Verifying properties of well-founded linked lists
• Verification, Model Checking, and Abstract Interpretation
• A Reachability Predicate for Analyzing Low-Level Software
• Foundations of Software Science and Computation Structures

This page was built for publication: Predicate abstraction for linked data structures

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