Les méthodes formelles sont un terme générique désignant des techniques rigoureuses de spécification et de vérification des systèmes informatiques, ou de construction de ces systèmes avec des garanties mathématiques sur leur exactitude ou sur l'absence de bugs.

Le model checking est un ensemble de techniques permettant de prouver formellement les propriétés d'un modèle donné, tandis que la synthèse de contrôleur consiste, à l'aide de techniques similaires, à compléter la description d'un système ouvert pour garantir une propriété donnée par construction.

L'une des cibles des méthodes formelles sont les systèmes présentant des aspects quantitatifs tels que les contraintes temps réel et les probabilités.

Dans cette thèse, je résume mes contributions sur des algorithmes de model checking et de synthèse de contrôleur pour des systèmes temporisés et probabilistes, en particulier, pour les formalismes des automates temporisés et des processus de décision de Markov.

You will find here the videos of past HDR defenses (2014 - 2023)

© 2023 Centre Inria de l’Université de Rennes