Résumé
Le cinquième séminaire a donné la parole à un des pionniers de l’interprétation abstraite mécanisée pour approfondir la vision simplifiée donnée dans le cinquième cours. Le conférencier a montré comment construire un interpréteur abstrait « correct par construction » à partir d’une sémantique collectrice pour le langage analysé et d’une bibliothèque compositionnelle de treillis complets. Il a ensuite décrit l’analyseur statique Verasco, qui est un interpréteur abstrait écrit et vérifié en Coq pour le langage intermédiaire C# du compilateur C vérifié CompCert, mettant en œuvre des domaines abstraits complexes pour les états mémoire et pour les nombres.
