Tahina Ramananandro

Welcome to my home page.

I am currently a post-doctoral associate within the FLINT team at Yale University.

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

My current research domain straddles Computer logic, Semantics of programming languages, machine-checked formal verification.

Contact

• Tahina.Ramananandro( chez )normalesup.org
  where you shall replace ( chez ) with the arobase @ (this is meant to trap spam bots). This is the most reliable way to contact me.
  
  
• Other options

Resume (curriculum vitae) (PDF)

Research topics

• 2008-2011 : Formal semantics of C++
• 2007 : Formal verification of memory managers (garbage collectors) (FR)
• 2006 : Mondex, an electronic purse: specification, refinement and proof with Alloy
• 2005 : Formal verification of probabilistic algorithms (FR)

Publications

• Tahina Ramananandro, Gabriel Dos Reis and Xavier Leroy
  A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management
  POPL 2012
  
  
• Tahina Ramananandro
  Mechanized Formal Semantics and Verified Compilation for C++ Objects
  Ph. D. thesis, University Paris. Diderot (Paris 7)
  Directed by Xavier Leroy, Gallium, INRIA Paris-Rocquencourt
  Successfully defended on January 10^th, 2012 at École normale supérieure.
  
  
• Tahina Ramananandro, Gabriel Dos Reis and Xavier Leroy
  Formal verification of object layout for C++ multiple inheritance
  POPL 2011
  
  
• Tahina Ramananandro
  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.