Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions: Technical Report

Wannes Tas; Bart Jacobs

doi:10.5281/zenodo.19254887

March 27, 2026Open Access

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions: Technical Report

View Full Paper

Ask AI

Bookmark

Share

Key Points

The aim is to define a program logic that effectively captures the pointer aliasing restrictions of Rust.
Defined a toy language to model Rust’s features.
Incorporated mutable and shared references along with UnsafeCell into the logic.
Detailed the representation of function arguments and two-phase borrows.
Presented a framework for verifying adherence to Rust's safety guarantees.
Demonstrated the ability to capture complex aliasing scenarios in a simplified setting.

Implication

Technical report defines a program logic to verify Rust’s pointer aliasing rules, highlighting implications for safety.

Abstract

This TR defines a program logic for a toy language that captures the following features of Rust’s pointer aliasing rules: mutable, references (including two-phase borrows), shared references, protection of function arguments, boxes, and UnsafeCell.

Discussion

No takes yet. Share an insight, caveat, or question.

Cite This Study

Tas et al. (2026) studied this question.

synapsesocial.com/papers/69c8c399de0f0f753b39e802 https://doi.org/10.5281/zenodo.19254887

View Full Paper

Ask AI

Bookmark

Share

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions: Technical Report

Key Points

Implication

Abstract

Discussion

Cite This Study

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions: Technical Report

Key Points

Implication

Abstract

Discussion

Cite This Study

Keep reading

Keep reading