About Me

I'm a research scholar (Chargé de recherche) in the Inria Épicure team (formerly Celtique), working on static analyses, program verification, program safety and security.

Before that, I was a research engineer at Prove & Run, working on the formal verification of the EAL7-certified ProvenCore μkernel (copy of the Common Criteria certificate).

I was a member of the DARPA-funded CRASH/SAFE program, working as a post-doctoral researcher under the supervision of Benjamin C. Pierce.

Formerly, I was a Ph.D. student in the Inria Gallium team, under the direction of Didier Rémy. My thesis was about the typing of ML modules. I defended my Ph.D. in 2010.

My research interests include: programming languages, semantics, formal methods, type systems, static analyses, program verification, non-interference, security monitors, information flow.



Recent software and mechanized proofs I have developed:

Not so recent sofware and proofs:


Please find below the list of my publications. Also please check out my entries on DBLP.


In academic year 2022-2023, I'm a teaching assistant for the following classes:


  • Address:

    Centre de recherche Inria Rennes Bretagne Atlantique
    Campus universitaire de Beaulieu
    35042 Rennes Cedex, France

  • Office: F 207
  • Email: benoit DOT montagu AT inria DOT fr
  • Phone: +33 (0) 2 99 84 74 55