Recherche


De l'interprétation algorithmique du blason

Système d'aide à la preuve

Preuves et Programmes

Certification et Logiciel critique

Terminaison de fonctions récursives

Le problème étudié est celui de la recherche automatique de preuve de terminaison de fonctions définies par un système d'équations récursives.
Nous restreignons la recherche à une certaine classe d'équations (grossièment : des fonctions définies par filtrage exhaustif sur ses arguments, sans utilisation du jocker (caractère _) Nous pouvons définir alors la notion d'arbre de distribution (grossièment : un arbre de filtrage dont chaque noeud est interprété comme l'application d'une règle de récurence structurelle) Le travail de thèse de Sylvain BARO a porté sur la Conception et implémentation d'un systéme d'aide à la spécification et à la preuve de programmes ML. Il y traite en particulier du problème de la terminaison.

Etudes de cas

L'art de la preuve de programme assistée par ordinateur a autant besoin de mise en pratique que d'investigation théorique. Il existe de multiples systèmes d'aide à la preuve basés sur divers formalismes : calcul des prédicats, théorie des types, réécriture, etc. Ces formalismes induisent autant des particularités des langage de spécification qu'ils proposent. Leur intégration dans un systéme d'aide à la preuve formelle offrent plus ou moins de souplesse dans la conduite ou le langage de preuve.
Il faut considérer cette diversité comme celle qui existe dans les langages de programmation. Un langage de spécification et le systéme de preuve associé ne doivent pas primer sur les concepts à mettre en oeuvre dans la modélisation. De même qu'un algorithme n'est pas tout à fait son implantation, une spécification doit être conçue à un niveau plus abstrait que celui de son codage dans tel ou tel formalisme. Par exemple : un prédicat, un type ou un ensemble sont des notions similaires. Toute spécification doit pouvoir être formulée en langue mathématique naturelle avant d'ètre formalisée pour tel ou tel système d'aide à la preuve.

Programmation

Collaborations ou contrats industriels

TICE


Page initiale Maison