Preuves, Programmes et Systèmes

27/11/2008 Éric Goubault (CEA LIST, MeASI)

Analyse statique de systèmes parallèles par des méthodes géométriques

Je décrirai dans cet exposé certains des principes sous-jacents de notre prototype d'analyseur statique ALCOOL (travail commun avec Emmanuel Haucourt, Michel Hirschowitz et Sanjeevi Krishnan). ALCOOL prend en entrée un programme écrit dans dans un langage intermédiaire traduisant l'essentiel des primitives de synchronisation POSIX, et calcule un certain nombre de propriétés concernant les problèmes de coordination eventuels. L'analyseur repose sur des notions de "topologie algébrique dirigée", qui permettent de caractériser des rétracts utiles de l'espace d'état. Je concluerai par l'extension de cet analyseur au calcul d'invariants (en termes de valeurs de variables) de programmes parallèles.