Matière
Certification du logiciel
Description
Tout développement logiciel est confronté au défi d'éviter les bugs ou, après coup, de vérifier leur absence. L’objectif de cette U.E. est de présenter différentes techniques permettant de garantir la correction d'un logiciel avec un bon degré de confiance. On présentera la sémantique des langages de programmation, aussi bien du point de vue opérationnel qu’axiomatique (Logique de Hoare).
Nous utiliserons l’assistant de preuves Coq pour décrire formellement ses sémantiques ainsi que leurs propriétés. Nous implanterons quelques programmes simples dans ce cadre.
Compétences requises
Preuves assistées par ordinateur
Notion de programmation, notamment fonctionnelle
Logique
Compétences visées
À l'issue de cet enseignement, un étudiant est capable de :
Décrire la sémantique d’un langage de programme
Écrire une spécification formelle d’un programme
Utiliser un outil comme Coq pour démontrer des propriétés de programmes en logique de Hoare
Discipline(s)
- Informatique
Syllabus
Outils pour garantir la fiabilité du logiciel.
Approche formelle et utilisation du logiciel Coq.
Descriptions formelles des sémantiques opérationnelles (petits pas et grands pas) et de la sémantique axiomatique
Lien entre ces deux types de sémantique
Exemples de preuves en logique de Hoare
Implantation de la logique de Hoare en Coq et preuves formelles de programmes simples
Approches alternatives pour garantir la fiabilité du logiciel
Bibliographie
Benjamin Pierce et al. Software Foundations. Volume 2 : Programming Language Foundations
Benjamin Pierce et al. Software Foundations. Volume 5 : Verifiable C