Shape Analysis for Composite Data Structures

DOI10.1007/978-3-540-73368-3_22MaRDI QIDQ5429321zbMATH OpenOpenAlexFDO

Authors Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Thomas Wies, Hongseok Yang, Peter W. O'Hearn

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_22

Mathematics Subject Classification ID

Data structures (68P05)

Recommendations

• A Shape Analysis for Non-linear Data Structures
• Shape analysis of low-level C with overlapping structures
• Relational inductive shape analysis
• Shape analysis of sets
• scientific article; zbMATH DE number 1953039

Cited in

(38)

• Unified reasoning about robustness properties of symbolic-heap separation logic
• Fragment abstraction for concurrent shape analysis
• Scalable Shape Analysis for Systems Code
• Shape Analysis by Graph Decomposition
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• scientific article; zbMATH DE number 1953039 (Why is no real title available?)
• scientific article; zbMATH DE number 56337 (Why is no real title available?)
• Towards dynamic shaping
• Foundations for entailment checking in quantitative separation logic
• Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• scientific article; zbMATH DE number 7361354 (Why is no real title available?)
• Reasoning about sequences of memory states
• Shape analysis of sets
• Shape neutral analysis of graph-based data-structures
• A Shape Analysis for Non-linear Data Structures
• Lightweight Separation
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Programs with lists are counter automata
• Shape analysis of low-level C with overlapping structures
• Footprints in Local Reasoning
• A divide-and-conquer approach for analysing overlaid data structures
• Program Verification with Separation Logic
• Lightweight shape analysis based on physical types
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Formal study of functional orbits in finite domains
• Reasoning about memory layouts
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• scientific article; zbMATH DE number 1940294 (Why is no real title available?)
• Separation Logic Tutorial
• Compositional entailment checking for a fragment of separation logic
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Tractable Reasoning in a Fragment of Separation Logic
• Forest automata for verification of heap manipulation
• Learning shape analysis
• Compositional shape analysis by means of bi-abduction
• A Logic-Based Framework for Reasoning about Composite Data Structures

Describes a project that uses

Uses Software

• TVLA

This page was built for publication: Shape Analysis for Composite Data Structures

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