Résumé
Dans ce premier séminaire de l'année, il a été question de la mise en œuvre mécanisée des logiques de programmes pour les logiciels écrits dans le langage C au moyen de Frama-C/WP.
Loïc Correnson a abordé la difficulté de maîtriser la complexité du calcul de plus faible précondition – weakest precondition calculus ou « wp » – et l’importance du modèle mémoire et de la simplification des obligations de preuve. Du point de vue de l’utilisateur, il a présenté les grandes approches méthodologiques permettant de s’attaquer industriellement à la preuve de programmes complexes.
Enfin, il a posé la question de la « qualité » d’une preuve et de sa base de confiance, ce qui lui a permis finalement de revisiter de manière surprenante la dualité test & preuve.
