Séminaire VASCO - Pierre LERMUSIAUX

Résumé :
La gestion d'exceptions est une fonctionnalité majeure des langages de programmation modernes. Les exceptions peuvent être utilisées pour gérer des erreurs et/ou comme des constructions contrôlant le flot d'exécution d'un programme. Une exception mal-rattrapée peut cependant conduire à l'arrêt inattendu du programme, et constitue donc un problème de sécurité majeur.Dans le cadre du projet Salto, nous avons conçu un analyseur statique permettant de détecter les exceptions non rattrapées dans les programmes fonctionnels. L'analyseur s'appuie sur le formalisme d'Interprétation Abstraite pour calculer, de manière simultanée, une description des valeurs potentiellement renvoyées et des exceptions potentiellement levées par un programme. L'interpréteur abstrait proposé a été implémentépour l'analyse statique de programmes OCaml, en couvrant ungrand nombre des fonctionnalités haut-niveau de ce langage, comme les types de données mutables, le système de modules 
et les types de données extensibles (dont les exceptions).