École CEA-EDF-Inria

Modélisation et vérification d'algorithmes en Coq : une introduction

Cette école CEA-EDF-Inria abordera les techniques de base en modélisation et vérification d'algorithmes en Coq. Elle s'adresse aux étudiants, chercheurs ou ingénieurs qui ont une bonne connaissance de la programmation dans un langage conventionnel (C, Java).

  • Date : 7/06/2010 au 11/06/2010
  • Lieu : Inria - Rocquencourt bâtiment 1
  • Organisateurs : Yves Bertot, Pierre Castéran, Pierre Letouzey, Assia Mahboubi

Objectifs :

Le système Coq fournit un langage de programmation fonctionnelle et un cadre de raisonnement basé sur la logique d'ordre supérieur pour effectuer des preuves sur les programmes. Le pouvoir expressif du langage est tel que l'on peut envisager des preuves sur des notions de mathématiques très avancées (comme le théorème des 4 couleurs) ou des programmes de complexité importante (comme un compilateur pour un noyau significatif du langage C). Dans ce cours, nous aborderons les techniques de base de la programmation dans ce langage et de la démonstration sur les programmes obtenus. Les concepts abordés seront : programmation récursive structurelle, manipulations de listes et d'entiers, démonstration par récurrence, définition récursive de types de données, constructions de filtrage et raisonnement par cas, propriétés inductives.

Programme :

Les cours commenceront lundi 7 à 10h, et se termineront vendredi 11 juin  à 16h.

Lundi 

Eléments de programmation fonctionnelle typée : programmation sans effets de bord, filtrage, fonctions anonymes, types prédéfinis simples nombres, booléens, listes, éléments de programmation d'ordre supérieure. Programmation récursive simple sur les nombres et les listes: introduction à la récursion structurelle

Mardi

Construction et preuves de formules logiques : quantificateurs et connecteurs logiques, égalité, prédicats prédéfinis sur les nombres et les listes. Démonstration de formules simple en Coq: preuve dirigée par les buts

Mercredi

Vérification de formules logiques simples concernant des programmes Preuves par récurrence sur les nombres et les listes. Nouveaux types de données et nouveau principes de raisonnement associés

jeudi

Prédicats inductifs et introduction aux types dépendants. Preuves par récurrence sur les prédicats inductifs. Fonctions à type dépendant, filtrage avec type dépendant

Vendredi

Combinaisons de types de données et de propriétés logiques Types portant des informations logiques Récursion généralisée

Mots-clés : Méthodes formelles Assistant de preuve Coq Algorithmes

Haut de page

Siège et centres de recherche Inria

Accès direct




Social