Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

DOI10.1007/11823230_13zbMath1225.68069OpenAlexW1887332367MaRDI QIDQ3613386

Cristiano Calcagno, Dino Distefano, Hongseok Yang, Peter W. O'Hearn

Publication date: 12 March 2009

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11823230_13

Mathematics Subject Classification ID

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

Related Items (6)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Unnamed Item ⋮ Concrete Memory Models for Shape Analysis ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• ASTREE

This page was built for publication: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic