Séance de cours
Cette séance de cours par l'instructeur plonge dans le concept d'invariants dans un système de compteur borné, en explorant les propriétés satisfaites par des états atteignables et la notion d'invariants inductifs. À travers des exemples et des exercices, la séance de cours démontre comment les invariants inductifs renforcent la compréhension du comportement du système et aident à prouver l'exactitude des propriétés. La séance de cours couvre également l'application pratique des invariants dans la vérification des comportements du système et l'importance d'algorithmes tels que la vérification des modèles bornés et la vérification des modèles à l'aide de diagrammes de décision binaires.