Romain Bardou INRIA engineer at LSV, SECSI team Mail: my firstname at my lastname dot fr

PhD thesis

I did my PhD from septembre 2007 to octobre 2011 at INRIA Saclay - Île-de-France with Claude Marché, in the ProVal team.

Title : Vérification de programmes avec pointeurs à l'aide de régions et de permissions
Download the abstract, the thesis or the slides.

See also Capucine.

Projects

• I contribute to Tookan, a tool for Cryptoki analysis.
• Capucine, a prototype implementation of my PhD work: a region and permission type system for deductive verification.
• Melt allows to write LaTeX documents using OCaml. It is composed of a library to produce .tex files, and of a preprocessor providing a syntax to mix OCaml and LaTeX. See slides.
• Fury Puyo is a free clone of Puyo Puyo, a fast and addictive puzzle game. It is coded using OCaml and uses the OCamlSDL library.
• I contribute to Mlpost, an OCaml librairy to produce LaTeX figures using Metapost.

Publications

[4]	Romain Bardou and Claude Marché. Perle de preuve : les tableaux creux. In Vingt-deuxièmes Journées Francophones des Langages Applicatifs (JFLA'11) [ bib | pdf ]
[3]	Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Technical Report RR-7414, INRIA, 2010. [ bib | pdf ]
[2]	Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane Lescuyer. Faire bonne figure avec Mlpost. In Vingtièmes Journées Francophones des Langages Applicatifs (JFLA'09) [ bib | pdf ]
[1]	Romain Bardou. Ownership, Pointer Arithmetic and Memory Separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib | pdf | pdf (long) | pdf (slides) ]

Presentations

• Introduction to Functional Programming Using OCaml, or: trying to convert chemists from Fortran to OCaml, 6 July 2011 for LCT, Jussieu.
• Regions and Permissions for Data Invariants, presentations of my PhD work, 14 January 2011 for INRIA teams Typical and ProVal.
• Melt: LaTeX with OCaml, presentation of Melt, my tool for writing LaTeX documents in OCaml.
• Regions and Permissions for Data Invariants, presentation of my PhD work, 2 November 2009 in Eindhoven for COST action FVOOS, as well as at the ProVal team meeting, 25 September 2009.
• Capacités, invariants et régions abstraites (in French), presentation of my PhD work, 13 March 2009 for ARC INRIA CeProMi.
• If you only knew the power of the Darcs side... (in French), a presentation of the distributed version manager Darcs.
• Regional Logic et Dynamic Frames (in French), a presentation of the dynamic frames of Ioannis T. Kassios and of the regional logic of Anindya Banerjee et al.

Internships

• March-July 2007: Class invariants and ownership systems, at INRIA Futurs (now INRIA Saclay - Île-de-France), with Claude Marché
  • Summary (in French)
  • Report (in French)
  • Presentation (in French)
• April-August 2006: Unions of abstract polymorphic variants, at Nagoya University (Japan), with Jacques Garrigue
  • Report (in French)
  • Presentation
• June-July 2005: Typing of recursive modules in Caml, at LIP, with Tom Hirschowitz
  • Report (in French)
  • Presentation (in French)