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)

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

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)