A shape graph logic and a shape system
type: Item
instance of: scholarly article
title: A shape graph logic and a shape system
zbMATH Open document ID: 1296.68100
author: Zhao-Peng Li
author: Yu Zhang
author: Yi-Yun Chen
published in: Journal of Computer Science and Technology
publication date: 2014-10-07T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6351820
zbMATH Keywords: shape graph logic
zbMATH Keywords: program verification
zbMATH Keywords: shape analysis
zbMATH Keywords: automated theorem proving
zbMATH Keywords: loop invariant inference
describes a project that uses: z3
describes a project that uses: Ynot
describes a project that uses: Isabelle
describes a project that uses: jStar
describes a project that uses: Spec#
describes a project that uses: ESC/Java
describes a project that uses: Smallfoot
MaRDI profile type: Publication
full work available at URL: s11390-013-1398-1
OpenAlex ID: W1985313353
cites work: Isabelle. A generic theorem prover
cites work: Ynot
cites work: Pointer Logic for Verification of Pointer Programs
cites work: Verifying properties of well-founded linked lists
cites work: Back to the future
cites work: A Logic-Based Framework for Reasoning about Composite Data Structures
cites work: Decidable logics combining heap structures and data
cites work: Separation and information hiding
cites work: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
cites work: Programming Languages and Systems
cites work: Relational inductive shape analysis
cites work: Separating Shape Graphs
cites work: Q2754081
cites work: Counterexample-guided focus
cites work: Recursive proofs for inductive tree data-structures
cites work: Compositional shape analysis by means of bi-abduction
DOI: 10.1007/S11390-013-1398-1
description: scientific article; zbMATH DE number 6351820