Interprocedural Shape Analysis with Separated Heap Abstractions

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

Mathematics Subject Classification ID

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