Nathalie Bertrand - Examinatrice
  Christel Baier - Rapporteuse
  Véronique Bruyère - Examinatrice
  Thomas Colcombet - Examinateur
  Javier Esparza - Rapporteur
  Jérôme Leroux - Rapporteur

Résumé: Model-checking is a verification technique which is in the past has been successfully applied to verify automatically the behavior of finite state systems. This approach consists in modelling a computing system by a mathematical model, in translating its specification into a logical formalism and then in proposing algorithms to check whether a model satisfies a logical formula. When the considered models have an infinite number of states, this method can easily lead to undecidable model-checking problems and one has hence to find the right trade-off between the expressiveness of models and specification languages and the feasibility of the verification. In this thesis, I present my contributions to the field of verification of infinite states systems where I have considered two main families of models. The first one are counter systems which can be seen as programs manipulating variables (called counters) taking their value in the natural. The second one are parameterised networks which can be seen as an abstraction of distributed networks where the number of participating entities is not fixed a priori and is unbounded. For these different models, I study exhaustively when the automatic verification is feasible and in the positive cases I try to design model-checking algorithms with optimal complexity bounds.

Plus d'informations disponibles sur la page web suivante :

https://www.irif.fr/~sangnier/hdr.html