Vous pouvez trouver ici les TD du cours d'initiation à la vérification donné en M1 à l'ENS Paris-Saclay.

• TD 1 : Logiques temporelles. [ corrigé ]
• TD 2 : Expressivité de LTL. [ corrigé ]
• TD 3 : Automates de Büchi. [ corrigé ]
• TD 4 : Automates de Büchi & CTL. [ corrigé ]
• TD 5 : Bisimulation & CTL.