Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 2, bâtiment C
                             Lundi 30 mai, 10h30

                               Aurèle Barrière
                                    IRISA

               Un compilateur Just-In-Time formellement vérifié
                     générant dynamiquement du code natif

Les compilateurs à la volée modernes choisissent d'optimiser
dynamiquement certaines fonctions fréquemment appelées. Pour des
raisons d'efficacité, ces compilateurs JIT ont souvent recours à un
backend pour générer du code natif correspondant aux fonctions à
optimiser. Un tel compilateur JIT doit alors entremêler interprétation
du code non compilé, compilation dynamique de certaines fonctions et
exécution de code natif. Cet exposé présente nos travaux en cours pour
réaliser un compilateur JIT formellement vérifié en Coq utilisant
CompCert comme backend pour générer du code natif. La preuve de
correction du JIT peut alors réutiliser la preuve de correction de
CompCert. L'exposé présentera nos solutions pour contourner les
limites de l'extraction Coq, du fait de la manipulation impure de la
pile d'exécution et de l'appel de code natif généré.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn