Separation logics and modalities: a survey

DOI10.1080/11663081.2015.1018801zbMath1398.03151OpenAlexW2041030963MaRDI QIDQ4586138

Morgan Deters, Stéphane P. Demri

Publication date: 12 September 2018

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.2015.1018801

zbMATH Keywords

computational complexitymodal logicfirst-order logictemporal logicsecond-order logicexpressive powerseparation logic decidability

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Temporal logic (03B44)

Related Items (10)

On a graph calculus for modalities ⋮ A First-Order Logic with Frames ⋮ Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ Exponential-Size Model Property for PDL with Separating Parallel Composition ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ On Temporal and Separation Logics ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition ⋮ Unnamed Item ⋮ Copy and remove as dynamic operators

Uses Software

• z3
• Smallfoot
• Infer
• Slide
• SeLoger

Cites Work

• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• An axiomatic basis for computer programming
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Foundations of Software Science and Computational Structures
• Mechanizing Mathematical Reasoning
• Impossibility of an algorithm for the decision problem in finite classes
• Tools and Algorithms for the Construction and Analysis of Systems
• Foundations of Software Science and Computation Structures
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maintaining knowledge about temporal intervals
• On the almighty wand
• Reasoning about sequences of memory states
• Elements of finite model theory.
• Expressiveness and complexity of graph logic
• An automata-theoretic approach to constraint LTL
• Proof methods for modal and intuitionistic logics
• Undecidability results on two-variable logics
• Finite-memory automata
• Multi-dimensional modal logic
• Many-dimensional modal logics: theory and applications
• The genesis of possible worlds semantics
• The price of universality
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Deterministic propositional dynamic logic: finite models, complexity, and completeness
• A logical characterization of data languages.
• Bunched logics displayed
• The semantics and proof theory of the logic of bunched implications
• First-order logic with two variables and unary temporal logic
• Relationships between nondeterministic and deterministic tape complexities
• Hybrid logics: characterization, interpolation and complexity
• Complexity Hierarchies beyond Elementary
• A Simple Separation Logic
• Separation Logic Modulo Theories
• LTL with the freeze quantifier and register automata
• Two-variable logic on data words
• Nondeterministic Phase Semantics and the Undecidability of Boolean BI
• Two-Variable Separation Logic and Its Inner Circle
• Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability
• Tractable Reasoning in a Fragment of Separation Logic
• Satisfiability Modulo Theories
• Future-Looking Logics on Data Words and Trees
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Undecidability of Propositional Separation Logic and Its Neighbours
• Context logic as modal logic
• A completeness theorem in modal logic
• Temporal logic can be more expressive
• A Reduction from DLP to PDL
• Tableaux and Resource Graphs for Separation Logic
• A Modal BI Logic for Dynamic Resource Properties
• Verifying Heap-Manipulating Programs in an SMT Framework
• Scalable Shape Analysis for Systems Code
• A Marriage of Rely/Guarantee and Separation Logic
• On the Almighty Wand
• On the Complexity of Reasoning About Dynamic Policies
• An Introduction to Context Logic
• On the Expressive Power of Graph Logic
• Separating Graph Logic from MSO
• Beyond Shapes: Lists with Ordered Data
• Using the Universal Modality: Gains and Questions
• The modal logic of inequality
• Methods for Automated Theorem Proving in Nonclassical Logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• The Logic of Bunched Implications
• On the Decision Problem for Two-Variable First-Order Logic
• A decision procedure for satisfiability in separation logic with inductive predicates
• Decidability of weak logics with deterministic transitive closure
• Expressive completeness of separation logic with two variables and no separating conjunction
• One-dimensional fragment of first-order logic
• The Expressive Power of Modal Dependence Logic
• The Tree Width of Separation Logic with Recursive Definitions
• Separation Logic with One Quantified Variable
• Global and Local Graph Modifiers
• Anytime, anywhere
• BI as an assertion language for mutable data structures
• Propositional Dynamic Logic with Storing, Recovering and Parallel Composition
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Compositional shape analysis by means of bi-abduction
• Permission accounting in separation logic
• Finite state machines for strings over infinite alphabets
• Foundations of Software Science and Computation Structures
• Computer Science Logic
• Computer Science Logic
• Computer Science Logic
• Compositional Invariant Checking for Overlaid and Nested Linked Lists
• A Proof of Kamp's theorem
• Parametric completeness for separation theories
• Proof search for propositional abstract separation logics via labelled sequents
• A proof system for separation logic with magic wand
• Decidable logics combining heap structures and data

This page was built for publication: Separation logics and modalities: a survey