Amphi C002 - Bâtiment Ampère de l'Ensimag
12 December 2024 - 15h00
Logics for Reasoning about the Correctness of Reconfigurable Distributed Systems (Phd Defense)
Lucas Bueri from Verimag
12 December 2024 - 15h00
Logics for Reasoning about the Correctness of Reconfigurable Distributed Systems (Phd Defense)
Lucas Bueri from Verimag
Abstract: Distributed computing is increasingly used, and requires regular modifications to remain efficient. However it can be penalizing or impossible to stop such systems, hence the use of dynamic reconfiguration. As this is a major source of errors, the need for modelling and verification is essential, and this is what we aim to contribute with our logical framework.
This thesis develops the Separation Logic of Relations (SLR) as a solution to describe reconfigurable distributed models through a set of inductive definitions. The local properties from separation logic help to develop techniques to address standard decision problems such as satisfiability, degree boundedness, or entailment of formulas. For the latter, the use of suitable restrictions on SLR was necessary to obtain decidability results without losing too much expressiveness. This led to significant work on both the treewidth boundedness and the MSO-definability of SLR models.
Jury :
- Stéphane Demri (Laboratoire Méthodes Formelles (LMF), rapporteur)
- Parthasarathy Madhusudan (University of Illinois at Urbana-Champaign, rapporteur)
- Nicolas Peltier (Laboratoire d'Informatique de Grenoble (LIG), examinateur)
- Anca Muscholl (Laboratoire Bordelais de Recherche en Informatique (LaBRI), examinatrice)
- Mihaela Sighireanu (Laboratoire Méthodes Formelles (LMF), examinatrice)
- Radu Iosif (Laboratoire VERIMAG, directeur de thèse)
- Marius Bozga (Laboratoire VERIMAG, co-directeur de thèse)
Remote link:
https://univ-grenoble-alpes-fr.zoom.us/j/92447986958?pwd=asMdwmCCgIRi2vJef4kkSElqNRvJLn.1
