Idée d'interprétation abstraite

Cette séance de cours introduit le concept d'interprétation abstraite comme méthode pour déduire les propriétés des calculs de programme. Il couvre l'idée de base, les états abstraits, les points fixes, les graphiques de flux de contrôle et les ensembles d'états aux points de programme. La séance de cours traite également de la preuve à travers des points fixes de fonctions approximatives, d'états accessibles en tant qu'équations récursives et de domaines d'analyse. Il explique l'approximation des ensembles, les fonctions de transfert et la mise à jour des ensembles dans le contexte de la signification du programme et des équations récursives.