Difference between revisions of "Cachan, April 29th and 30th"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 19: | Line 19: | ||
being related to modal separation logics. Part of the presented work is done | being related to modal separation logics. Part of the presented work is done | ||
jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba). | jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba). | ||
| + | |||
'''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities'' | '''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities'' | ||
Revision as of 18:58, 19 March 2019
Stephane Demri: Modal Separation Logics and Friends
Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative models is a feature shared with many modal logics such as sabotage logics, logics of public announcements or relation-changing modal logics. In the first part of the talk, we present several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. In the second part of the talk, we present the decidability status and the computational complexity of several modal separation logics, (for instance, leading to NP-complete or Tower-complete satisfiability problems). In the third part, we investigate the complexity of fragments of quantified CTL under the tree semantics (or similar modal logics with propositional quantification), some of these fragments being related to modal separation logics. Part of the presented work is done jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).
Alessio Mansutti: Axiomatising Logics with Separating Conjunction and Modalities
Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics MSL(*,<=/=>) and MSL(*,<>), where * is the separating conjunction, <> is the standard modal operator and <=/=> is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.
