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
- Xavier Denis, Jacques-Henri Jourdan. "Specifying and Verifying Higher-order Rust Iterators." International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023 [pdf (preprint)]
- Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. "Creusot: a Foundry for the Deductive Verification of Rust Programs." Formal Methods and Software Engineering: 23rd International Conference on Formal Engineering Methods, ICFEM 2022 [pdf
- 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