On temporal and separation logics

DOI10.4230/LIPICS.TIME.2018.1zbMATH Open1487.68080OpenAlexW2990336109MaRDI QIDQ5079764FDOQ5079764

Authors: Stéphane Demri 

Publication date: 28 May 2022

Full work available at URL: https://hal.science/hal-02366656

Recommendations

• Separation logics and modalities: a survey
• The effects of modalities in separation logics (extended abstract)
• Temporal and dynamic logic
• Logics in computer science. A study on extensions of temporal and strategic logics
• Program Verification with Separation Logic

zbMATH Keywords

expressive powertemporal logicsseparation logics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70)

Cites Work

• Expressiveness and completeness of an interval tense logic
• The semantics and proof theory of the logic of bunched implications
• The Logic of Bunched Implications
• Title not available (Why is that?)
• BI as an assertion language for mutable data structures
• An axiomatic basis for computer programming
• The Expressive Power of Modal Dependence Logic
• A Modal Logic for Chopping Intervals
• Tools and Algorithms for the Construction and Analysis of Systems
• A Simple Separation Logic
• Separation logics and modalities: a survey
• Title not available (Why is that?)
• Scalable Shape Analysis for Systems Code
• Automated Theorem Proving for Assertions in Separation Logic with All Connectives
• Separating Graph Logic from MSO
• On the almighty wand
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Reasoning about sequences of memory states
• Expressiveness and complexity of graph logic
• Foundations of Software Science and Computational Structures
• The Tree Width of Separation Logic with Recursive Definitions
• Quantified CTL: Expressiveness and Complexity
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Compositional Shape Analysis by Means of Bi-Abduction
• Title not available (Why is that?)
• Decidable and undecidable logics with a binary modality
• The effects of adding reachability predicates in propositional separation logic
• A decision procedure for satisfiability in separation logic with inductive predicates
• Parametric completeness for separation theories
• Title not available (Why is that?)
• Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
• Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
• Two-Variable Separation Logic and Its Inner Circle
• Title not available (Why is that?)

Cited In (3)

• Separation -- past, present, and future
• Correction
• A temporal logic for sortals

Uses Software

• Smallfoot
• Viper
• Infer
• Slide
• SeLoger

This page was built for publication: On temporal and separation logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5079764)