Sujets de stage

L'objectif du projet PROTHEO est la conception et la réalisation d'outils pour la spécification, la preuve et la vérification de logiciels. Calcul et déduction sont exprimés à l'aide des concepts de règles, de contraintes et de stratégies. Ce formalisme déclaratif et exécutable permet la spécification, le prototypage, et la vérification de composants logiciels. Nous développons un environnement de prototypage et des techniques de preuve adaptés pour vérifier des propriétés de ces programmes.

Nos recherches s'appuient sur trois domaines scientifiques: contraintes, réécriture et mécanisation de la déduction. Ces trois thèmes se fertilisent mutuellement dans le projet. En particulier, nous utilisons les contraintes et les techniques de réécriture pour améliorer l'efficacité des démonstrateurs et nous formalisons les solveurs de contraintes et les démonstrateurs à l'aide de règles contrôlées par des stratégies.

Les logiciels développés dans le projet (ELAN, TOM, Cariboo, GasEl) nous servent à valider nos idées, à présenter nos travaux à la communauté scientifique et à transférer nos connaissances vers des domaines d'applications.

Le stage de 4 mois suivant concerne les étudiants d'écoles d'ingénieurs étrangers

Les stages de Master suivants sont une initiation à la recherche dans le cadre de l'équipe et sont tous susceptibles d'un prolongement en thèse.