Concrete memory models for shape analysis

DOI10.1016/J.ENTCS.2010.09.012MaRDI QIDQ2814114zbMATH OpenOpenAlexFDO

Authors Pascal Sotin, Bertrand Jeannet, Xavier Rival

Publication date 17 June 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2010.09.012

zbMATH Keywords

C-like programming languagesmemory modelsprogramming language semanticsshape analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A concrete memory model for CompCert
• Separating shape graphs
• Region-based shape analysis with tracked locations
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• scientific article; zbMATH DE number 1953039

Cites work

• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Mechanized semantics for the clight subset of the C language
• Relational inductive shape analysis
• Separating shape graphs
• Shape analysis of low-level C with overlapping structures

Cited in

(3)

• Lightweight shape analysis based on physical types
• Symbolic memory with pointers
• Separating shape graphs

This page was built for publication: Concrete memory models for shape analysis

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