Xavier Denis

I'm a PhD student at the LMF — under the supervision of Jacques-Henri Jourdan and Claude Marché — where I study the deductive verification and specification of Rust programs.

My objective is to show that the verification of low-level software can be made more tractable by leveraging the Rust type system. This work encompasses both the theoretical and applied aspects of the question. As part of this work I am developing Creusot, a deductive verifier for Rust built on top of Why3.

Contact: email


  1. Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer. RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2022. [pdf]
  2. Denis, Xavier. "Mastering Program Verification using Possession and Prophecies." 32 ème Journées Francophones des Langages Applicatifs: 174.
  3. Denis, Xavier. Deductive program verification for a language with a Rust-like typing discipline. Diss. Université de Paris, 2020.