Rust is a relatively new programming language for writing performant code with strong type and memory safety guarantees. It has become a serious competitor to C and C++ for systems programming, because it provides high-level abstractions but without the cost of garbage collection. Given the growing popularity of Rust, and given that bugs in systems programs can be costly, there is growing interest in the program verification community for building program verifiers for Rust. In this fourth workshop in the series, we aim to continue the conversation among language designers, application developers and formal verification tool builders, to exchange ideas and build collaborations around developing verified Rust programs.
The goal of the workshop is to bring together researchers from a variety of different backgrounds and perspectives to exchange new and exciting ideas concerning the verification of Rust programs and explore potential avenues for collaboration.
We would like the workshop to be informal and interactive. The program will thus involve a combination of invited talks, contributed talks about work in progress, tool demos, and open discussion sessions. There will be no published proceedings, but participants will be encouraged to submit working documents, talk slides, etc. to be posted on this website.
Building on the success of the first four Rust Verification workshops (virtually in 2021, and in-person in 2022, in 2023 and in 2024), we are once again expanding the workshop to span 2 days.
Organizers ⸺ rw2025-organizers@googlegroups.com
Rajeev Joshi, Amazon Web Services <jorajeev@amazon.com>
Felix Klock <pnkfelix@pnkfx.org>
Andrea Lattuada, Max Planck Institute for Software Systems <andrea@mpi-sws.org>
Alex Summers, The University of British Columbia, <alex.summers@ubc.ca>