Asma Tafat: Preuves par raffinement de programmes avec pointeurs. (Proofs by refinement of programs with pointers). University of Paris-Sud, Orsay, France 2013