Xavier Denis, Jacques-Henri Jourdan and their co-authors Yusuke Matsushita and Derek Dreyer received a Distinguished Paper Award for their contribution RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code at PLDI 2022, the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation.
PLDI is "the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance". It is one of the four prestigious conferences of SIGPLAN, ACM's special interest group on programming languages. Each year, among the 60-80 papers presented at the conference, only a few are selected to receive the distinguished paper award, based on their quality, and RustHornBelt is one of them for the year 2022!
In a machine-checked proof in Coq, RustHornBelt shows how the type system of the Rust programming language can be used to generate simple verification conditions which can be used to prove the functional correctness of Rust programs. It is a generalization of the previous work RustBelt, which proved sound the type system of Rust using logical relations in the Iris separation logic in 2017. However, RustHornBelt adds an essential feature by allowing typing judgements to provide functional specifications to terms as first-order logical formulas with prophecy variables. These formulas are particularly well-suited for functional verification because they do not require any reasoning about pointer aliasing even if the program manipulates pointers. In addition, RustHornBelt inherits an essential feature of RustBelft: it can be extended to prove correct functional specifications of unsafe Rust code, which makes this result easier to use in practice.
The award-winning contribution serves as a theoretical foundation for the Creusot tool that Xavier Denis is developing for the deductive verification of Rust programs, together with his PhD advisors Jacques-Henri Jourdan and Claude Marché.