Octagon Abstract Interpreter: Mise en oeuvre des programmes C

Cette séance de cours porte sur la mise en oeuvre d'un interprète abstrait d'Octagon pour les programmes C. Il explique l'arrière-plan de l'interprétation abstraite et des octogones, le domaine octogone, les contraintes octogonales, la représentation de la matrice DBM, les fermetures et différents types de fermetures comme le chemin le plus court, les fermetures fortes et serrées. La séance de cours traite également de la durée des fermetures, de l'interprétation abstraite en arrière, de l'évaluation des expressions dans le domaine abstrait, du traitement des pointeurs, de l'analyse FrontC, et se termine par l'état d'avancement et les travaux futurs du projet.