Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Abstract
The type system of Rust enforces the “shared xor mutable” principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of interior mutability. Thus, supporting interior mutability in a deductive verification tool is difficult. The Verus tool demonstrated the use of ghost resources to that end. So far, this mechanism has only been applied to Verus in order to verify primarily system code.
Fields of Study & Subjects
Sports Analytics and Performance
Merger and Competition Analysis
Wine Industry and Tourism
Publication details
- Journal / source
- Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs
- Publisher
- ACM
- Pages
- 383–397
- Publication date
- 8 January 2026
- Language
- EN