Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908920957632512 |
|---|---|
| author | Tas, Wannes Jacobs, Bart |
| author_facet | Tas, Wannes Jacobs, Bart |
| contents | 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 exploited by the Rust compiler to generate more efficient machine code, and enforced by Rust's static type system, except inside unsafe blocks. In this paper, we present our work in progress towards the first program logic for modularly verifying that Rust programs that use unsafe blocks comply with the pointer-aliasing rules. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_28326 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions Tas, Wannes Jacobs, Bart Programming Languages 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 exploited by the Rust compiler to generate more efficient machine code, and enforced by Rust's static type system, except inside unsafe blocks. In this paper, we present our work in progress towards the first program logic for modularly verifying that Rust programs that use unsafe blocks comply with the pointer-aliasing rules. |
| title | Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2603.28326 |