Aller au contenu  Aller au menu Aller à la recherche

accès rapides, services personnalisés

Rechercher

Recherche détaillée

Contact

Jacqueline Collet-Narboni
Responsable administrative

courriel : jacqueline.collet-narboni@upmc.fr

Cette page est la page de garde du site consacré à l' unité d'enseignement « Spécification et Validation de Programmes (5I554) »

Ressources annuelles

Responsable de l'UE : MANOURY, pascal


Site de l'UE

Description de l'UE :

Ce cours aborde le thème de la spécification et vérification des programmes sous l'angle de l'utilisation de théories et de langages logiques tels la théorie des ensembles et la logique d'ordre supérieur. Les spécifications sont données comme des formules logiques; les vérifications sont des preuves que les formules de la spécification sont satisfaites par un programme donné ou un programme à construire. Pour conduire ces preuves, nous nous appuierons sur les systèmes d'aide à la preuve tels PVS, Coq, Isabelle/HOL ou autre.