MSM

Imprimer

MSM : Mechanized Semantics

Responsable : Sandrine Blazy (mail)

Équipe pédagogique : Sandrine Blazy et David Pichardie (mail)

Description

La justification rigoureuse d'un travail scientifique est une part importante dans l'activité de recherche en informatique. Ce cours part du constat que certains étudiants éprouvent des difficultés a réaliser eux-mêmes une argumentation rigoureuse, en grande partie par manque de pratique durant leurs études antérieures. Le cours a pour but de rappeler les éléments de base pour réaliser une preuve rigoureuse et encadrer un travail personnel permettant à l'étudiant de réaliser ses propres preuves. Le cours s'appuie sur deux cas d'études issues du monde de la recherche :

  • Assistant de preuve : les preuves peuvent être réalisées à l'aide d'un outil comme Coq (http://coq.inria.fr) qui se charge de vérifier la correction de chaque étape élémentaire du raisonnement. Ce cours n'est pas un cours sur Coq à proprement parler. Seuls certaines parties de l'outil seront présentées afin de permettre à l'étudiant d'utiliser l'outil pendant son travail personnel. Les cours magistraux s'appuieront sur cet outil et les étudiants seront encouragés à utiliser leurs machines personnelles pendant ces cours.
  • Sémantique des langages de programmation : l'étude des sémantiques a pour but de donner une description mathématique précise sur le comportement attendu des programmes écrit dans un langage donné. Elle permet notamment de justifier rigoureusement la correction d'un compilateur en démontrant qu'un programme source et un programme cible obtenu par compilation auront les même comportements observables. Les preuves réalisées dans ce cours auront pour objet d'étude différentes formes de sémantique pour différents paradigmes de programmation (impératif, objet, parallèle).

Le cours s'appuiera sur l'utilisation d'un forum de discussion. Les étudiants seront invités à compléter les cours par des discussions sur ce forum.

Le cours se terminera par une présentation des travaux de recherche au sujet d'une sémantique formelle réaliste pour le langage C, écrite avec l'outil Coq (cf. http://compcert.inria.fr).

Keywords: preuve sur machine, sémantique des langages de programmation

Prerequisites: notions de programmation fonctionnelle, cours de compilation, cours de logique niveau Licence

Savoir et savoir faire associés

  • Ecriture d'une preuve rigoureuse et correcte.
  • Notions élémentaires en preuve assistée
  • Description rigoureuse du comportement attendu d'un programme
  • Etude méta-théorique de différents paradigmes de programmation

Structure générale et contenu

  • Découverte de l'assistant de preuve Coq
  • Raisonnement par induction sur les entiers et les listes
  • Modélisation d'un mini langage : syntaxe et sémantique
  • Preuves de propriétés sémantiques
  • Vérification d'un mini-compilateur

Le cours est composé de 14h de cours magistral et de 6h de suivi de projet.

Références bibliographiques

  • Pierce B.C.  Software Foundations
  • Nielson H.R., Nielson F. Semantics with applications: A formal introduction. Wiley, 1992

Modalités d'évaluation

  • Un projet personnel (30%) + 1 examen terminal (70%)
Buy cheap web hosting service where fatcow web hosting review will give you advices and please read bluehost review for more hosting information.