Pierre Wilke

Address: Bureau F214, Irisa/Inria
Campus de Beaulieu
263, avenue du général Leclerc
35042 RENNES Cedex - France
Email: pierre.wilke@irisa.fr

I am a PhD student in the Celtique team at Université de Rennes 1 in France. My PhD work is about certified compilation of low-level programs.

My research interests cover the topics of static analysis of programs, low-level code and proof methods.

A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data with S. Blazy and F. Besson.
Submitted for publication in Special Issue for ITP'15 in the Journal of Automated Reasoning (JAR).
A Concrete Memory Model for CompCert with S. Blazy and F. Besson. [slides]
In Interactive Theorem Proving (ITP'15), LNCS 9236, Springer 2015.
A Precise and Abstract Memory Model for C using Symbolic Values with S. Blazy and F. Besson. [slides]
In Asian Symposium on Programming Languages and Systems (APLAS'14), LNCS 8858, Springer 2014.

In 2014/2015, I am teaching the following lab sessions: