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
- 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]
- Denis, Xavier. "Mastering Program Verification using Possession and Prophecies." 32 ème Journées Francophones des Langages Applicatifs: 174.
- Denis, Xavier. Deductive program verification for a language with a Rust-like typing discipline. Diss. Université de Paris, 2020.