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:
- The slide deck for the training courses for
agrégation
d'informatique I gave at ENS Rennes
(2021-2023) on the topic of "Programming
languages" (in French) is now available!
[ Page of the course (in French) ] - The paper "Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation" (with Pierre Lermusiaux) has been accepted at ESOP2024!
- The Salto project on defining sound static analyses for OCaml programs is about to start! This project is part of a partnership between Inria and Nomadic Labs, and is funded by the Tezos Foundation.
- The paper "Lifting Numeric Relational Domains to Algebraic Data Types" (with Santiago Bautista and Thomas Jensen) has been accepted at SAS2022!
- The paper "Trace-Based Control-Flow Analysis" has been accepted at PLDI'21! Check out the associated demo!
- Check out the demo associated to the ICFP 2020 paper "Stable Relations and Abstract Interpretation of Higher-Order Programs"! The page features the static analyzer that is described in the paper. It should run in your browser out of the box.
SOFTWARE
Recent software and mechanized proofs I have developed:
-
dmap: an OCaml library that implements dependent (heterogeneous) maps. The types of the values recorded in such maps may depend on the values of the keys. Yet, they are type safe.
[ Repository ] -
sexp_decode: an OCaml library of monadic combinators for decoding S-expressions (as defined in the Csexp library) into structured data.
[ Repository ] -
Control-flow analyzers for the
λ-calculus: prototype analyzers that
accompany the PLDI'21
paper "Trace-Based Control-Flow
Analysis". Includes the ∇-CFA,
widening-based, control-flow analysis. Written
in OCaml.
[ Demo | Sources ] -
A relational analyzer for the
λ-calculus: prototype analyzer that
accompanies the ICFP'20
paper "Stable
Relations and Abstract Interpretation of
Higher-Order Programs". Infers
stable relations between the inputs and the
outputs of a program. Written
in OCaml.
[ Demo | Sources ] -
Formal proofs on stable
relations: Coq
formalization that accompanies the ICFP'20
paper "Stable
Relations and Abstract Interpretation of
Higher-Order Programs".
[ Documentation | Sources ]
Not so recent sofware and proofs:
-
Coq
formalization that accompanies the CSF'13
article "A
Theory of Information-Flow
Labels".
[ Sources ] -
Coq
formalization of the
article "Robust
Declassification" by Zdancewic
and Myers.
[ Repository ] -
Coq
formalization of Core F-zip, the language
I developed as part of
my Ph.D.
thesis, that features the
open existential types I introduced in
the POPL'09
paper "Modeling
Abstract Types in Modules with Open Existential
Types". I described some
aspects of this development at
the Workshop
on Mechanized Metatheory (2010).
[ Repository ] -
Prototype typechecker for F-zip,
the language I developed as part of
my Ph.D.
thesis. It is a core language for modules. It
features polymorphism, open existential types,
singleton kinds, and subtyping, and is explicitly
typed. Written
in OCaml.
[ Repository ]
TEACHING
In academic year 2024-2025, I participate to the following classes:
- 1st
semester: Software
Analysis and Security (SOS). In collaboration
with Thomas
Jensen
and Benjamin
Farinier. (Lectures, Master 2)
Keywords: operational semantics, static analysis for safety and security, abstract interpretation. - 1st
semester: Analyse
et Conception Formelles (ACF). "Software
Formal Analysis and Design", supervised
by Thomas
Genet. (Lab sessions, Master 1)
Keywords: formal specifications, verification, interactive theorem proving, Isabelle. - 2nd
semester: Programmation
de confiance (PRGC). "Trustworthy programming",
supervised
by Sandrine
Blazy. (Lab sessions, Licence 3)
Keywords: formal specifications, verification, deductive verification, Why3.
Contacts
- 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
- ORCID iD:
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