Modèles formels de calcul et leurs applications

cherchez ici le projet détaillé (postscript)

Modèles du Parallèlisme et Applications

L'avènement des réseaux et des systèmes distribués a entrainé un besoin grandissant de formalismes de modélisation et de programmation, qui soient fondés sur l'étude théorique des processus parallèles (ou «concurrency theory» en anglais).

Les travaux actuels de nos groupes s'orientent vers la modélisation de la mobilité, initiée par le pi-calcul, vers l'unification de principes issus des programmations fonctionnelle et concurrente, ainsi que vers l'étude de systèmes de type adaptés aux processus parallèles.

L'équipe Meije développe le calcul bleu, en poursuivant l'étude des propriétés et du typage de termes du pi-calcul. L'équipe Para développe le join-calcul. L'équipe de Huimin Lin à Institut du Logiciel de l'Académie des Sciences de Beijing étudie les méthodes et outils de preuve pour les calculs de processus avec communication de messages ou de canaux.

Modèles abstraits de calculs séquentiels et parallèles

Théorie des Types et de la Preuve

Raisonnement automatique

Zhang Jian de l'Institut du Logiciel applique la génération de modèles finis à la vérification de programmes. Il expérimente l'utilisation d'outils logiciels définis dans un cadre de raisonnement automatique pour la résolution de systèmes d'équations booléennes positives, qui apparaissent naturellement dans des contexts de vérification de programmes matériels ou logiciels.

Coordinateurs

Gérard Boudol 
projet Meije 
INRIA Sophia-Antipolis		 Huimin Lin 
Software Institute, Beijing 
Chinese Science Academy
 

Autres participants

Robert de Simone

Last modified: Fri Dec 5 11:03:44 MET