Pierre Kimmel (Types team) will defend his thesis on Thursday, December 6th at 10am in room B013.

His presentation is entitled “Modal extensions of resource logics : expressiveness and calculi”.

The jury members are  :

• Nicolas Olivetti, Professeur Université Aix-Marseille, LSIS, Marseille
• Serenella Cerrito, Professeur Université Evry Val d’Essonne, IBISC, Evry
• David Pym, Professeur University College London, Londres
• Hans van Ditmarsch, Directeur de recherche CNRS, LORIA, Nancy
• Didier Galmiche, Professeur Université de Lorraine, LORIA, Nancy
• Dominique Larchey-Wendling, Chargé de recherche CNRS, LORIA, Nancy

Abstract :

The design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently.

We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics.
A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives intemporal branching modelling, allowing for instance to characterize multi-thread processes.
A complementary study concerns the modelling of access by agents to properties under the conditions of
posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems.
In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the
internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and
HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the
axiomatisation of BBI logic and some of its variants.
In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part
of this thesis is dedicated to the definition of proof calculi, here tableaux calculi, for those new logics, as well as
their proofs of soundness and completeness.