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 retrace cette évolution des idées et présente, conjointement avec le séminaire, un certain nombre de résultats récents dans le domaine.
Les enregistrement vidéo sont disponibles sur le site du Collège de France.
Une partie du cours est formalisée dans l'assistant à la démonstration Coq. Les sources Coq commentés sont disponibles depuis le projet cdf-program-logics.
Certains exposés étaient en français, d'autres en anglais. Les enregistrements vidéo et les présentations sont disponibles sur le site du Collège de France.
Xavier.Leroy@college-de-france.fr