Martin Pépin (LIP6, Paris)

En programmation concurrente, l’ordre d’exécution des actions d’un programme n’est pas entièrement spécifié. En conséquence, le nombre d’exécutions possibles d’un programme croît rapidement avec la taille du programme et on assiste alors le célèbre phénomène ``d’explosion combinatoire’’. Ce phénomène est un obstacle aux nombreuses techniques d’analyse existantes. Pour parer à ce problème, notre approche consiste à adopter un point de vue probabiliste en générant des exécutions possibles uniformément au hasard, permettant ainsi d’explorer efficacement l’espace d’état du programme.

Dans cet exposé, je présenterai un cadre pour l’étude des programmes concurrent ainsi que quelques sous classes de programmes pour lesquelles nous avons pu développer des algorithmes efficaces de génération aléatoire uniforme d’exécutions. Je présenterai ensuite un de ces algorithme, qui couvre la plupart des classes présentées dans l’exposé.