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.