A shape graph logic and a shape system

DOI10.1007/s11390-013-1398-1zbMath1296.68100OpenAlexW1985313353MaRDI QIDQ744329

Zhao-Peng Li, Yu Zhang, Yi-Yun Chen

Publication date: 7 October 2014

Published in: Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11390-013-1398-1

zbMATH Keywords

automated theorem provingshape analysisprogram verificationloop invariant inferenceshape graph logic

Mathematics Subject Classification ID

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

Uses Software

• Isabelle
• Spec#
• z3
• ESC/Java
• Smallfoot
• jStar
• Ynot

Cites Work

• Unnamed Item
• Isabelle. A generic theorem prover
• Recursive proofs for inductive tree data-structures
• Pointer Logic for Verification of Pointer Programs
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Back to the future
• Relational inductive shape analysis
• Separation and information hiding
• Separating Shape Graphs
• Ynot
• Counterexample-guided focus
• Compositional shape analysis by means of bi-abduction
• Programming Languages and Systems
• Verifying properties of well-founded linked lists
• Decidable logics combining heap structures and data
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

This page was built for publication: A shape graph logic and a shape system