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

Disciplines

• 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

Contacts

Responsable(s) de l'enseignement

• Nicolas Magaud