Publications : Xavier Denis
Retour| [6] | Xavier Denis. Deductive Verification of Rust Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib | full text on HAL ] |
| [5] | Xavier Denis and Jacques-Henri Jourdan. Specifying and verifying higher-order rust iterators. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 13994 of Lecture Notes in Computer Science, pages 93--110. Springer, 2023. [ bib | DOI | full text on HAL ] |
| [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.