Abstract FR:

Pour modéliser les systèmes parallèles et communicants, on utilise les algèbres de processus introduites par R. Milner permettant de donner la sémantique de termes représentant de tels systèmes sous forme de systèmes de transitions. Pour vérifier des programmes, on utilise la notion d'équivalence observationnelle associée à un critère d'observation. Le système AUTO issu du système ECRINS qui permet de manipuler des algèbres de processus est utilisé pour la mise en œuvre du principe de vérification. On donne une description complète du système et de son implantation en LE LISP. Son utilisation est illustrée par des exemples très classiques dans le domaine de la vérification des systèmes parallèles. On traite ensuite des exemples plus complexes d'algorithmes distribués