Evènement pour le groupe GT Génie Logiciel

Date 2012-05-02  13:00-14:00
TitreA formally verified SSA-based middle-end - Static Single Assignment meets CompCert. 
RésuméCompCert is a formally verified compiler that generates compact and efficient PowerPC, ARM and x86 code for a large and realistic subset of the C language. However, CompCert foregoes using Static Single Assignment (SSA), an intermediate representation that allows for writing simpler and faster optimizers, and is used by many compilers. In fact, it has remained an open problem to verify formally a SSA-based middle-end compiler. We report on a formally verified, SSA-based, middle-end for CompCert. Our middle-end performs conversion from CompCert intermediate form to SSA form, optimization of SSA programs, including Global Value Numbering, and transforming out of SSA to intermediate form. In addition to provide the first formally verified SSA-based middle-end, our work addresses two problems raised by Leroy: giving a simple and intuitive formal semantics to SSA, and showing how to leverage the global properties given by SSA to reason locally about program optimizations. 
LieuSalle Ada Lovelace, Bât. A29 
OrateurDelphine Demange 
UrlEquipe Celtique, Inria Rennes 

Aucun document lié à cet événement.

Retour à l'index