Verification of multi-linked heaps

DOI10.1016/j.jcss.2011.08.003zbMath1246.68093MaRDI 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

verification; trees; model checking; termination; abstraction; shape analysis; small model; heaps; lists; ranking abstraction

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

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

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