Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions
The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or borrowed as read-only through one or more shared references. These rules, known as Rust's pointer-aliasing rules, are e...
Shranjeno v:
| Autores principales: | , |
|---|---|
| Format: | Artículo |
| Izdano: |
2026
|
| Teme: | |
| Online dostop: | https://arxiv.org/abs/2603.28326 http://arxiv.org/abs/2603.28326 |
| Oznake: |
Brez oznak, prvi označite!
|
Podobne knjige/članki: Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions
- Modular Formal Verification of Rust Programs with Unsafe Blocks
- Verifying Probabilistic Programs in Rust
- Annotating and Auditing the Safety Properties of Unsafe Rust
- RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
- UnsafeChecker: Finding Soundness Bugs in Rust Safe Abstractions
- An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model