A shape graph logic and a shape system

DOI10.1007/S11390-013-1398-1MaRDI QIDQ744329zbMATH OpenOpenAlexFDO

Authors 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

shape analysisprogram verificationautomated theorem provingloop invariant inferenceshape graph logic

Mathematics Subject Classification ID

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

Recommendations

• Programming Languages and Systems
• Relational and Kleene-Algebraic Methods in Computer Science
• Shape Analysis by Graph Decomposition
• Automated Verification of Shape and Size Properties Via Separation Logic
• Graph-based shape analysis beyond context-freeness

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Back to the future, revisiting precise program verification using SMT solvers
• Compositional shape analysis by means of bi-abduction
• Counterexample-guided focus
• Decidable logics combining heap structures and data
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Isabelle. A generic theorem prover
• Pointer logic for verification of pointer programs
• Programming Languages and Systems
• Recursive proofs for inductive tree data-structures
• Relational inductive shape analysis
• Separating shape graphs
• Separation and information hiding
• Verifying properties of well-founded linked lists
• Ynot: dependent types for imperative programs

Cited in

(12)

• Learning shape analysis
• Relational and Kleene-Algebraic Methods in Computer Science
• Shape Analysis by Graph Decomposition
• Computer Aided Verification
• scientific article; zbMATH DE number 1629942 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation
• Abstraction of object graphs in program verification
• Automated Verification of Shape and Size Properties Via Separation Logic
• A relational framework for higher-order shape analysis
• Shape neutral analysis of graph-based data-structures
• Programming Languages and Systems
• Reasoning about memory layouts

Describes a project that uses

Uses Software

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

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

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