Relational inductive shape analysis

DOI10.1145/1328438.1328469MaRDI QIDQ3189844zbMATH OpenOpenAlexFDO

Authors Bor-Yuh Evan Chang, Xavier Rival

Publication date 12 September 2014

Published in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1328438.1328469

zbMATH Keywords

heap analysisinductive definitionsmaterializationseparation logicshape analysissymbolic abstract domain

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Analysis of algorithms and problem complexity (68Q25) Semantics in the theory of computing (68Q55)

Recommendations

• A relational framework for higher-order shape analysis
• Shape analysis with reference set relations
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Graph-based shape analysis beyond context-freeness
• Learning shape analysis
• Shape-similarity relations based on topological resolution
• Inference and learning with hierarchical shape models
• scientific article; zbMATH DE number 4119686

Cited in

(22)

• Bunched logics displayed
• A relational shape abstract domain
• A generic framework for heap and value analyses of object-oriented programming languages
• Concrete memory models for shape analysis
• A relational framework for higher-order shape analysis
• Invariants synthesis over a combined domain for automated program verification
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Shape analysis of sets
• Reduced product combination of abstract domains for shapes
• Verification of heap manipulating programs with ordered data by extended forest automata
• A unified display proof theory for bunched logic
• Galois Connections for Recursive Types
• Shape analysis with reference set relations
• Discovering invariants via simple component analysis
• Automated cyclic entailment proofs in separation logic
• Semantic-directed clumping of disjunctive abstract states
• Shape Analysis for Composite Data Structures
• Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning
• Sound Automation of Magic Wands
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• An array content static analysis based on non-contiguous partitions
• A shape graph logic and a shape system

This page was built for publication: Relational inductive shape analysis

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