Vérification formelle d'une plate-forme d'exécution Java: premiers résultats et perspectives

Nous nous intéressons aux compilateurs optimisants formellement vérifiés avec un assistant de preuve. Dans ce domaine, le compilateur CompCert pour le langage C fait date: il a été programmé et prouvé correct avec l'assistant de preuve Coq. Nous listerons le chemin qu'il reste à accomplir pour étendre ces travaux à des langages plus haut-niveaux comme Java, en insistant plus particulièrement sur la représentation intermédiaire de programme SSA (Static Single Assignment) privilégiée par les compilateurs optimisants modernes. Nous verrons qu'un compilateur de ce type révèle de nombreux challenges en termes de sémantique, d'analyses statiques et de preuves de programme.