Séminaire des équipes de recherche
A Formal C Memory Model Supporting Integer-Pointer Casts
- 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.