View source for Cachan, April 29th and 30th

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.