About Me

I'm a research scientist in the Inria Celtique team, working on static analyses, program verification, and security. I hold a Starting Research Position (SRP), which is a 3-year research position.

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.

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 2020-2021, I'm a teaching assistant for the following classes:


  • Address:

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

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