Collocated Events

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 fifth 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.

The 32nd International SPIN symposium on Model Checking of Software (SPIN 2026) will be held in Turin, Italy, during ETAPS 2026. SPIN 2026 is the latest in a successful series of workshops and symposia for practitioners and researchers interested in symbolic and state space-based techniques for the validation and analysis of software systems. Techniques and empirical evaluations based on explicit representations of state spaces, as implemented in the SPIN model checker or other tools, or techniques based on the combination of explicit representations with other representations, are the focus of this symposium.