Sites Inria

English version

Séminaire des équipes de recherche

A Formal C Memory Model Supporting Integer-Pointer Casts

© INRIA Sophie Auvin - G comme Grille

  • Date : 23/02/2016
  • Lieu : Salle de réunion Jacques-Louis Lions 1, bâtiment C
  • Intervenant(s) : Chung-Kil Hur (Seoul National University)

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.

Mots-clés : Séminaire Gallium Formal C Memory Supporting Integer-Pointer Casts Model

Haut de page

Suivez Inria