Interprocedural Shape Analysis with Separated Heap Abstractions

DOI10.1007/11823230_16MaRDI QIDQ3613389zbMATH OpenOpenAlexFDO

Authors Alexey Gotsman, Josh Berdine, Byron Cook

Publication date 12 March 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11823230_16

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

Recommendations

• scientific article; zbMATH DE number 1693492
• Static Analysis
• Static Analysis
• Interprocedural shape analysis for effectively cutpoint-free programs
• Heap Decomposition for Concurrent Shape Analysis
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Hierarchical shape abstraction for analysis of free list memory allocators

Cited in

(27)

• Interprocedural shape analysis using separation logic-based transformer summaries
• Fragment abstraction for concurrent shape analysis
• Hierarchical shape abstraction for analysis of free list memory allocators
• scientific article; zbMATH DE number 1693492 (Why is no real title available?)
• Spatial interpolants
• Invariants synthesis over a combined domain for automated program verification
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Precise interprocedural side-effect analysis
• Barriers in Concurrent Separation Logic
• Precise interprocedural analysis in the presence of pointers to the stack
• Access analysis-based tight localization of abstract memories
• Heap Decomposition for Concurrent Shape Analysis
• Lightweight Separation
• Separating shape graphs
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Interprocedural shape analysis for effectively cutpoint-free programs
• Compositional shape analysis by means of bi-abduction
• Region-based shape analysis with tracked locations
• Calling context abstraction with shapes
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Static Analysis
• Static Analysis
• Separation Logic Tutorial
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Summarization for termination: No return!

This page was built for publication: Interprocedural Shape Analysis with Separated Heap Abstractions

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