Certification du logiciel

Certification du logiciel
Master InformatiqueParcours Science et ingénierie du logiciel (SIL)

ComposanteUFR de mathématique et d'informatique

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 axiomatiqueLien entre ces deux types de sémantiqueExemples de preuves en logique de HoareImplantation de la logique de Hoare en Coq et preuves formelles de programmes simplesApproches 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