Relational inductive shape analysis

DOI10.1145/1328438.1328469zbMath1295.68081OpenAlexW2013050211MaRDI QIDQ3189844

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

shape analysisheap analysisseparation logicinductive definitionsmaterializationsymbolic abstract domain

Mathematics Subject Classification ID

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

Related Items (13)

A generic framework for heap and value analyses of object-oriented programming languages ⋮ Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ Verification of heap manipulating programs with ordered data by extended forest automata ⋮ A Unified Display Proof Theory for Bunched Logic ⋮ Bunched logics displayed ⋮ Discovering invariants via simple component analysis ⋮ Galois Connections for Recursive Types ⋮ An array content static analysis based on non-contiguous partitions ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ A shape graph logic and a shape system ⋮ Concrete Memory Models for Shape Analysis ⋮ A relational shape abstract domain ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification

This page was built for publication: Relational inductive shape analysis