A semantics for procedure local heaps and its abstractions

DOI10.1145/1040305.1040330MaRDI QIDQ5276154zbMATH OpenOpenAlexFDO

Authors Noam Rinetzky, J. Bauer, Mooly Sagiv, Reinhard Wilhelm, Thomas Reps

Publication date 14 July 2017

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

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

zbMATH Keywords

3-valued logicabstract interpretationshape analysisstatic analysis

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 7149819
• Static Analysis
• Algebraic Methodology and Software Technology
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Automatic numeric abstractions for heap-manipulating programs

Cited in

(9)

• Interprocedural shape analysis using separation logic-based transformer summaries
• Establishing local temporal heap safety properties with applications to compile-time memory management
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Inference of field-sensitive reachability and cyclicity
• Unbounded allocation in bounded heaps
• Access analysis-based tight localization of abstract memories
• scientific article; zbMATH DE number 2090863 (Why is no real title available?)
• Interprocedural shape analysis for effectively cutpoint-free programs
• Separation Logic Tutorial

This page was built for publication: A semantics for procedure local heaps and its abstractions

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