Comment valider un logiciel ? Revenir à l'accueil

Xavier Leroy, professeur titulaire de la chaire "Sciences du logiciel", introduit son cours de l'année 2020-2021 : "Logiques de programmes : quand la machine raisonne sur ses logiciels". Accéder à la suite de cet enseignement : https://www.college-de-france.fr/site...​ 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.