Interprocedural Shape Analysis with Separated Heap Abstractions
From MaRDI portal
Publication:3613389
DOI10.1007/11823230_16zbMath1225.68072OpenAlexW2160563691MaRDI QIDQ3613389
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
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (10)
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ Summarization for termination: No return! ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Lightweight Separation ⋮ Barriers in Concurrent Separation Logic ⋮ Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ Access Analysis-Based Tight Localization of Abstract Memories ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Separation Logic Tutorial
This page was built for publication: Interprocedural Shape Analysis with Separated Heap Abstractions