Difference between revisions of "Cachan, April 29th and 30th"

From Numerical Transition Systems
Jump to: navigation, search
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.