On temporal and separation logics

DOI10.4230/LIPICS.TIME.2018.1MaRDI QIDQ5079764zbMATH OpenOpenAlexFDO

Authors Stéphane Demri

Publication date 28 May 2022

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

zbMATH Keywords

expressive powerseparation logicstemporal logics

Mathematics Subject Classification ID

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

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

Cites work

• A decision procedure for satisfiability in separation logic with inductive predicates
• A Modal Logic for Chopping Intervals
• A simple separation logic
• An axiomatic basis for computer programming
• Automated theorem proving for assertions in separation logic with all connectives
• BI as an assertion language for mutable data structures
• Compositional shape analysis by means of bi-abduction
• Decidable and undecidable logics with a binary modality
• Decidable logics with associative binary modalities
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressiveness and completeness of an interval tense logic
• Expressiveness and complexity of graph logic
• Extending propositional separation logic for robustness properties
• Foundations of Software Science and Computational Structures
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 6131597 (Why is no real title available?)
• Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
• On the almighty wand
• On the complexity of modal separation logics
• Parametric completeness for separation theories
• Quantified CTL: expressiveness and complexity
• Reasoning about sequences of memory states
• Scalable Shape Analysis for Systems Code
• Separating Graph Logic from MSO
• Separation logics and modalities: a survey
• The effects of adding reachability predicates in propositional separation logic
• The expressive power of modal dependence logic
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• The tree width of separation logic with recursive definitions
• Tools and Algorithms for the Construction and Analysis of Systems
• Two-Variable Separation Logic and Its Inner Circle
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(5)

• Separation -- past, present, and future
• Separation logics and modalities: a survey
• The effects of modalities in separation logics (extended abstract)
• A temporal logic for sortals
• Correction

Describes a project that uses

Uses Software

• Smallfoot
• Viper
• SeLoger
• Slide
• Infer

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)