Sujet : Sémantique des programmes par les jeux
Responsables : Pierre Castéran, Aymeric Vincent et Igor
Walukiewicz
Téléphone : 054000 (6931 | 3509 | 6903)
e-mail : Pierre Castéran, Aymeric
Vincent, Igor Walukiewicz
Équipe : Méthodes Formelles
Présentation du sujet : Il est de plus en plus admis que la
vérification de programmes ou de
systèmes informatiques a pour
préalable la compréhension de leur
sémantique,
c'est-à-dire une description
formelle de leur comportement et de
leur interaction avec leur
environnement. Cette connaissance est un
prérequis absolu pour valider ces
programmes, de façon plus ou
moins automatique.
Ce stage propose d'étudier la "Game semantics" des
programmes
impératifs, qui présente toute exécution
comme un dialogue
entre deux joueurs. Dans des cas particuliers, la sémantique d'un
programme peut se représenter par
un automate fini, ce qui rend
décidable le problème d'équivalence
de deux
programmes. Cependant, en vue de
traiter les programmes contenant des
variables ayant des domaines
infinis ou dont le traitement automatique
dépasserait les capacités de nos
machines, il est souhaitable de
manipuler cette sémantique avec des
outils de preuve, qui
requièrent une intervention humaine
pour prouver des
propriétés sur la sémantique d'un
programme, mais peuvent
traiter des programmes qui
autrement ne seraient pas traitables.
Le système Coq est un tel outil. La preuve d'une propriété de
programme se fait de façon assistée,
sous forme d'un dialogue
entre l'utilisateur qui établit des
stratégies de
démonstration, et le système qui
prend en charge les parties
calculatoires des preuves, ou enchaîne
de nombreuses inférences
logiques par l'intermédiaire de "tactiques"
programmables. Le
travail consiste en plusieurs tâches
:
- Comprendre la "Game
Semantics" et ses apports à la sémantique des langages
de
programmation
- Réaliser un développement en Coq permettant
d'exprimer la sémantique des
programmes d'un petit langage
impératif. Ce développement
contiendra des tactiques et
stratégies permettant de vérifier
le plus automatiquement
possible les propriétés de tel
programme ou classe de
programmes.
Mot-clés :
Jeux, sémantique, logique, systèmes d'aide à la démonstration.
Références :
Sur la sémantique par les jeux. S. Abramsky,
Algorithmic
Game Semantics: A Tutorial Introduction, in Proof and
System
Reliability, H. Schichtenberg and R. Steinbruggen, eds.,
Proceedings
of the NATO Advanced Study Institute, Marktoberdorf,
Kluwer Academic Publishers, 2001, 21--47.
Commentaires éventuels : Un sujet à la frontière entre
théorie et pratique. Compréhension
du domaine et
implémentation vont de pair.