Séance de cours
Cette séance de cours couvre l'encodage déterministe des systèmes de transition à l'état fini en utilisant des fonctions booléennes, représentant les fonctions booléennes avec des tables et des formules, la logique propositionnelle, les problèmes de satisfaction et les invariants inductifs dans les circuits séquentiels. Il traite également de la vérification limitée du modèle pour laccessibilité et les systèmes de preuve formels.