Wiki Agenda Contact English version

Publications : Xavier Denis

Retour
[5] Xavier Denis. Deductive Verification of Rust Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib ]
[4] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: a foundry for the deductive verication of Rust programs. In International Conference on Formal Engineering Methods - ICFEM, Lecture Notes in Computer Science, Madrid, Spain, 2022. Springer. [ bib | full text on HAL ]
Keywords: Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits
[3] Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In International Conference on Programming Language Design and Implementation, pages 841--856. ACM, 2022. [ bib | DOI | full text on HAL ]
[2] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. The Creusot environment for the deductive verification of Rust programs. Research Report 9448, Inria Saclay - Île de France, 2021. [ bib | full text on HAL ]
[1] Xavier Denis. Deductive program verification for a language with a Rust-like typing discipline. Internship report, Université de Paris, September 2020. [ bib | full text on HAL ]

Retour
This page was generated by bibtex2html.