Logiques de programmes : quand la machine raisonne sur ses logiciels

De même qu'une logique mathématique permet de démontrer des propriétés des objets mathématiques, une logique de programme permet de démontrer des propriétés d'un programme informatique et de toutes ses exécutions possibles. Apparues dans les années 1960 avec les travaux fondateurs de Floyd et de Hoare, les logiques de programmes se sont énormément développées depuis les années 2000, avec des avancées conceptuelles comme les logiques de séparation et de belles applications à la vérification déductive de logiciels critiques. Le cours retracera cette évolution des idées et présentera, conjointement avec le séminaire, un certain nombre de résultats récents dans le domaine.