Tahina Ramananandro

Welcome to my home page.

I am an alumnus of École normale supérieure, Paris, France, into which I was admitted in 2004 through exams.

Currently, I am a PhD student at INRIA Rocquencourt. My PhD project is directed by Xavier Leroy, head of the Gallium research team: formally verifying runtime systems and compilers for high-level programming languages.

In more detail, I plan to develop a static compiler for Java (à la GCJ) towards the PowerPC architecture, and to prove its semantics preservation using the Coq proof assistant. This property ensures that whenever a Java source code has a well-defined behaviour, then the PowerPC assembly code also has a well-defined behaviour and produces the same system calls as the original Java source code. The proof relies on Xavier Leroy's Compcert certified C-to-PowerPC compiler.

Resume

• My resume, also called Curriculum Vitae, in PDF format
  

Publications

• Mondex, an electronic purse : specification and refinement checks with the Alloy model-finding method
  FACJ (Formal Aspects of Computing journal), special issue 20.1, January 2008.
  The official version is available here at www.springer.com.

Internships

• The Mondex Case Study with Alloy
  The internship I followed at MIT, in the USA, from March 6th to August 26th, 2006. Its aim was to use the Alloy formal method to verify the specification of an electronic purse (also called smart card) system.

Contact

• Tahina.Ramananandro( chez )normalesup.org
  where you shall replace ( chez ) with the arobase @ (this is meant to trap spam bots).

Other stuff

• My website in French
  where you can discover much more of my research interests and other activities