Ce projet est un tutoriel qui explore les outils RV pour la vérification de programmes multithreadés. Il illustre les défis de la surveillance d'un programme parallèle en examinant l'interplay entre les exécutions de programmes et les formalismes de spécification. Le tutoriel utilise des moniteurs écrits manuellement avec AspectJ, Java-MOP, MarQ et Larva.