Verification of multi-linked heaps

DOI10.1016/j.jcss.2011.08.003zbMath1246.68093OpenAlexW1985592284MaRDI QIDQ439948

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

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

verificationtreesmodel checkingterminationabstractionshape analysissmall modelheapslistsranking abstraction

Mathematics Subject Classification ID

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

Uses Software

• JTLV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verification by augmented finitary abstraction
• A Logic-Based Framework for Reasoning about Composite Data Structures
• MODULAR RANKING ABSTRACTION
• Undecidability results on two-variable logics
• A combination framework for tracking partition sizes
• Computer Science Logic
• Computer Aided Verification
• Shape Analysis of Single-Parent Heaps
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Programs with Lists Are Counter Automata
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Foundations of Software Science and Computation Structures

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