Vérification automatique de systèmes infinis

Séminaire
  • Quand ? 06/10/2017 à partir de 14:00 (America/Montreal / UTC-400)
  • Où ? Au local D4-2011 de la Faculté des sciences
  • Participants Michael Blondin, candidat au poste de professeur au Département d’informatique
  • Ajouter l'événement au calendrier iCal

RÉSUMÉ : Dans cette présentation, nous verrons comment les méthodes formelles permettent d'automatiser la vérification du bon comportement de systèmes concurrents et distribués. En particulier, nous traiterons de la vérification de modèles (model checking), qui consiste à vérifier de façon algorithmique qu'un système satisfait une propriété donnée. Ces vérifications deviennent rapidement indécidables lorsque les systèmes considérés possèdent un nombre infini d'états. Nous verrons qu'il demeure malgré tout possible de décider plusieurs propriétés intéressantes de ces systèmes infinis en contrepartie d'un coût calculatoire considérable.

Dans cette optique, j'introduirai des formalismes répandus pour modéliser les systèmes infinis: réseaux de Petri, systèmes d'addition de vecteurs, protocoles de population, etc. Je ferai ensuite un survol de mes travaux récents portant sur l'algorithmique, la complexité et l'expressivité de ces formalismes. En particulier, j'expliquerai comment certaines de ces avancées permettent d'améliorer les capacités et les performances d'outils de vérification. Finalement, je discuterai de perspectives de recherche liées à cet exposé.

Toutes les personnes intéressées sont cordialement invitées.