Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C MARDI 23 février, 10h30 ------------- Chung-Kil Hur ------------- Seoul National University ======================================================== A Formal C Memory Model Supporting Integer-Pointer Casts ======================================================== In this talk, I will present our formal memory model for C-like languages that fully supports casts between integers and pointers. By "formal", we mean our model is fully formalized in Coq. By "full support", we mean our model allows almost all kinds of sensible casting (ie, casted pointers are just normal 32/64-bit integers), yet still validates almost all kinds of compiler optimizations. Finally, we strongly believe that our model is easily applicable to the CompCert compiler because our model is a slight variation of the CompCert C memory model. This work was published at PLDI 15 and more information can be found at the following page. http://sf.snu.ac.kr/intptrcast/