Partager cette page :

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

le 16 octobre 2012

de 15h30 à 17h00

ENS Rennes Salle du conseil
Plan d'accès

Intervention de David Pichardie, Inria Rennes / Harvard University. Séminaire du département Informatique et télécommunications.

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.
Thématique(s)
Formation, Recherche - Valorisation
Contact
François Schwarzentruber

Mise à jour le 9 septembre 2019