Completeness of cyclic proofs for symbolic heaps with inductive definitions
type: Item
instance of: scholarly article
title: Completeness of cyclic proofs for symbolic heaps with inductive definitions
zbMATH Open document ID: 1542.68038
DOI: 10.1007/978-3-030-34175-6_19
author: Makoto Tatsuta
author: Koji Nakazawa
author: Daisuke Kimura
publication date: 2024-04-19T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 7834983
MaRDI profile type: Publication
cites work: Foundations for Decision Problems in Separation Logic with General Inductive Predicates
cites work: Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
cites work: Q5144661
cites work: On the Almighty Wand
cites work: Relational inductive shape analysis
cites work: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
cites work: Programming Languages and Systems
cites work: Formalised Inductive Reasoning in the Logic of Bunched Implications
cites work: Sequent calculi for induction and infinite descent
cites work: Automated Cyclic Entailment Proofs in Separation Logic
cites work: A decision procedure for satisfiability in separation logic with inductive predicates
cites work: Model checking for symbolic-heap separation logic with inductive predicates
cites work: Automated verification of shape, size and bag properties via user-defined predicates in separation logic
cites work: Tractable Reasoning in a Fragment of Separation Logic
cites work: Compositional Invariant Checking for Overlaid and Nested Linked Lists
cites work: Compositional Entailment Checking for a Fragment of Separation Logic
cites work: The Tree Width of Separation Logic with Recursive Definitions
cites work: Deciding Entailments in Inductive Separation Logic with Tree Automata
cites work: Effective entailment checking for separation logic with inductive definitions
cites work: Separation Logic Modulo Theories
cites work: Cyclic Arithmetic Is Equivalent to Peano Arithmetic
cites work: Automated mutual explicit induction proof in separation logic
cites work: Separation Logic with Monadic Inductive Definitions and Implicit Existentials
description: scientific article; zbMATH DE number 7834983