scientific article; zbMATH DE number 2081098

zbMath1052.68590MaRDI QIDQ4474211

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn

Publication date: 4 August 2004

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2245/22450108.htm

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

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items (37)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Program Verification with Separation Logic ⋮ Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Trakhtenbrot’s Theorem in Coq ⋮ Being and Change: Reasoning About Invariance ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ A logic of reachable patterns in linked data-structures ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Expressiveness and complexity of graph logic ⋮ Relational separation logic ⋮ Separation logic with one quantified variable ⋮ Separation logics and modalities: a survey ⋮ Compositional entailment checking for a fragment of separation logic ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ On the almighty wand ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Reasoning about sequences of memory states ⋮ On the Almighty Wand ⋮ Lightweight Separation ⋮ Strong-separation logic ⋮ Elimination of spatial connectives in static spatial logics ⋮ Quantitative separation logic and programs with lists ⋮ Unnamed Item ⋮ Elimination of quantifiers and undecidability in spatial logics for concurrency ⋮ Unnamed Item ⋮ Beyond Shapes: Lists with Ordered Data ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition ⋮ Tractable Reasoning in a Fragment of Separation Logic ⋮ On Model Checking Boolean BI ⋮ Unnamed Item ⋮ Manipulating Trees with Hidden Labels ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

This page was built for publication: