Collège De France (sciences Et Technologies)

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Résumé Comment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme, via des raisonnements formels au sein d'une logique appropriée : une logique de programmes. Le premier cours a illustré cette approche par la vérification déductive d'une fonction de recherche dichotomique dans un tableau trié, un algorithme très utilisé et souvent implémenté de manière incorrecte. Ensuite, le cours a retracé l'émergence de la vérification déductive et des logiques de programmes via trois publications fondatrices. La brève communication d'Alan Turing en 1949, intitulée « Checking a large routine », int