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 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)

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

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 6131597 (Why is no real title available?)
• scientific article; zbMATH DE number 7561347 (Why is no real title available?)
• A Modal Logic for Chopping Intervals
• A decision procedure for satisfiability in separation logic with inductive predicates
• 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
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computational Structures
• 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 Logic of Bunched Implications
• The effects of adding reachability predicates in propositional separation logic
• The expressive power of modal dependence logic
• 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 logics and modalities: a survey
• Separation -- past, present, and future
• Correction
• The effects of modalities in separation logics (extended abstract)
• A temporal logic for sortals

Describes a project that uses

Uses Software

• SeLoger
• Slide
• Infer
• Viper
• Smallfoot

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)