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.


News:


SOFTWARE

Recent software and mechanized proofs I have developed:


Not so recent sofware and proofs:



PUBLICATIONS

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



TEACHING

In academic year 2024-2025, I participate to the following classes:


Contacts

  • Address:

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


    Show a larger map

  • Office: F 207
  • Email: benoit DOT montagu AT inria DOT fr
  • Phone: +33 (0) 2 99 84 74 55
  • ORCID iD: ORCID logo https://orcid.org/0009-0005-6153-6276
  • Affiliation: Univ Rennes, CNRS, Inria, IRISA (Institut de recherche en informatique et systèmes aléatoires) - UMR 6074, F-35000 Rennes