scientific article; zbMATH DE number 7350781

MaRDI QIDQ4989410

Daisuke Kimura, Makoto Tatsuta

Publication date: 25 May 2021

Full work available at URL: https://arxiv.org/abs/1802.05935

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

decidabilityarraysseparation logiclistsprogram analysis/verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (1)

Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps

Uses Software

• Predator
• Infer
• Slide

Cites Work

• Biabduction (and related problems) in array separation logic
• Compositional Entailment Checking for a Fragment of Separation Logic
• Tractable Reasoning in a Fragment of Separation Logic
• Back to the future
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• Separation Logic with Monadic Inductive Definitions and Implicit Existentials
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• A decision procedure for satisfiability in separation logic with inductive predicates
• The Tree Width of Separation Logic with Recursive Definitions
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Compositional Invariant Checking for Overlaid and Nested Linked Lists
• Compositional Shape Analysis by Means of Bi-Abduction
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: