Nicolas Waldburger's PhD defense
General information
The defense will take place in room Métivier (Inria Rennes) at 2pm on 11th December. It can be followed online at the following link.The current version of the thesis can be found here.
Composition of the jury
Reviewers before defense
Javier ESPARZA : Professeur, Technische Universität MünchenAntonín KUCERA : Professeur, Masaryk University, Brno
Jury
Examiner : Patricia BOUYER-DECITRE, Directrice de recherche, CNRS, LMF, ENS Paris-SaclayExaminer : Javier ESPARZA, Professeur, Technische Universität München
Examiner : Antonín KUCERA, Professeur, Masaryk University, Brno
Examiner : Nathalie SZNAJDER, Maîtresse de conférence, Sorbonne Université
Examiner : Igor WALUKIEWICZ, Directeur de recherche, CNRS, LaBRI, Université de Bordeaux
PhD director : Nathalie BERTRAND, Directrice de recherche, INRIA, Université de Rennes
PhD co-director : Nicolas MARKEY, Directeur de recherche, CNRS, IRISA, Université de Rennes
PhD supervisor : Ocan SANKUR, Chargé de recherche, CNRS, IRISA, Université de Rennes
Title and abstract
Title: Parameterized verification of distributed shared-memory systems
Abstract: Distributed systems consist in several computerized components (called processes) interacting with one another to perform a common task. An example of such a task is consensus, where all processes must agree on a common value. In this thesis, we are interested in shared-memory systems where the processes interact via reading from and writing to a shared memory. We do not work directly on distributed systems, but rather on models of such systems, and we consider questions related to the automated verification of these models. Our models are parameterized: the number of processes is not fixed beforehand and may be arbitrarily large, so that we are able to verify the system regardless of the number of participants. They enjoy some monotonicity property, called copycat property, which simplifies the analysis. Motivated by consensus algorithms from the literature, we consider a model where each process evolves incrementally in a number called round and where each round has its own set of registers. Also, we study the impact of a stochastic scheduler on this round-based model. Our approach is theoretical and we are mostly interested in analyzing our models and in classifying our problems of interest in terms of complexity.