Prepas.org

Le site de l'UPS pour les Classes Préparatoires aux Grandes Écoles

ENS Cachan Preuves de correction et de terminaison d'algorithmes le Vendredi 27 juin 2014


Preuves de correction d'algorithmes :
Comment savoir si un algorithme est correct ? Il y a deux aspects bien différents dans cette question, d'une part le problème de la terminaison de l'algorithme, et d'autre part celui de sa correction partielle : à chaque fois qu'il termine, est-ce que l'algorithme fait bien ce qu'on attend de lui (satisfait sa spécification). L'objectif de cette formation est de fournir les clés pour étudier la correction partielle des algorithmes.


Preuves de terminaison d'algorithmes :
Les preuves de terminaison des algorithmes s'appuient en général sur des notions fondamentales de théorie des ordres et de combinatoire : ordres bien fondés, calculs sur les ordinaux, etc. Le but de la formation proposée est de présenter ces notions fondamentales, de les illustrer sur quelques exemples tirés de l'informatique, et de fournir des pointeurs bibliographiques pour qui souhaiterait approfondir.

Session sur les Langages formels et applications, Bases de données relationnelles du 24 avril 2014 ici

Inscription en ligne : [ici-

http://www.dptinfo.ens-cachan.fr/LIESSE/] > Preuves de correction d'algorithmes
Paul Gastin, ENS Cachan
Vendredi 27 juin 2014, 10h–13h

Niveau de la formation : Informatique pour tous

Contenu : Exemples de preuves d'algorithmes, invariants. Logique de Hoare : sémantique, système de preuves, plus faible pré-condition. Exemples : boucles, procédures, récursivité.


Preuves de terminaison d'algorithmes
Philippe Schnoebelen, CNRS & ENS Cachan
Vendredi 27 juin 2014, 14h30–17h30

Contenu : quelques exemples de (non?)-terminaison ; ordres bien fondés, beaux préordres, ordinaux ; lemme de Higman, applications en théorie des langages ; théorème de Kruskal, théorème de Robertson-Seymour, applications en algorithmique des graphes.

Contacter le Département Informatique ici