Verification of multi-linked heaps

DOI10.1016/J.JCSS.2011.08.003MaRDI QIDQ439948zbMATH OpenOpenAlexFDO

Authors Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck

Publication date 17 August 2012

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jcss.2011.08.003

zbMATH Keywords

verificationshape analysistreesmodel checkingabstractionsmall modelterminationheapslistsranking abstraction

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Shape Analysis of Single-Parent Heaps
• Forest automata for verification of heap manipulation
• Verification, Model Checking, and Abstract Interpretation
• Verifying properties of well-founded linked lists
• Predicate abstraction for linked data structures

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 3735091 (Why is no real title available?)
• scientific article; zbMATH DE number 2080047 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• A Logic-Based Framework for Reasoning about Composite Data Structures
• A combination framework for tracking partition sizes
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Computer Aided Verification
• Computer Science Logic
• Foundations of Software Science and Computation Structures
• MODULAR RANKING ABSTRACTION
• Programs with Lists Are Counter Automata
• Shape Analysis of Single-Parent Heaps
• Undecidability results on two-variable logics
• Verification by augmented finitary abstraction
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(2)

• scientific article; zbMATH DE number 1956556 (Why is no real title available?)
• Shape Analysis of Single-Parent Heaps

Describes a project that uses

Uses Software

• JTLV

This page was built for publication: Verification of multi-linked heaps

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