Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Tas, Wannes, Jacobs, Bart
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model
by: Jacobs, Bart, et al.
Published: (2025)

NPB-Rust: NAS Parallel Benchmarks in Rust
by: Martins, Eduardo M., et al.
Published: (2025)

PermRust: A Token-based Permission System for Rust
by: Gehring, Lukas, et al.
Published: (2025)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
by: Wu, Jinhua, et al.
Published: (2026)

RustMC: Extending the GenMC stateless model checker to Rust
by: Pearce, Oliver, et al.
Published: (2025)

Auditing Rust Crates Effectively
by: Zoghbi, Lydia, et al.
Published: (2026)

Charon: An Analysis Framework for Rust
by: Ho, Son, et al.
Published: (2024)

Surveying the Rust Verification Landscape
by: Blanc, Alex Le, et al.
Published: (2024)

A flexible specification approach for verifying total correctness of fine-grained concurrent modules
by: Fasse, Justus, et al.
Published: (2023)

Towards a Transpiler for C/C++ to Safer Rust
by: Tripuramallu, Dhiren, et al.
Published: (2024)

VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs
by: Jacobs, Bart
Published: (2025)

Annotating and Auditing the Safety Properties of Unsafe Rust
by: Rao, Zihao, et al.
Published: (2025)

Cocoon: Static Information Flow Control in Rust
by: Lamba, Ada, et al.
Published: (2023)

An Interactive Debugger for Rust Trait Errors
by: Gray, Gavin, et al.
Published: (2025)

Garbage Collection for Rust: The Finalizer Frontier
by: Hughes, Jacob, et al.
Published: (2025)

&inator: Correct, Precise C-to-Rust Interface Translation
by: Chen, Victor, et al.
Published: (2026)

Crux, a Precise Verifier for Rust and Other Languages
by: Pernsteiner, Stuart, et al.
Published: (2024)

A Hybrid Approach to Semi-automated Rust Verification
by: Ayoun, Sacha-Élie, et al.
Published: (2024)

Scylla: Translating an Applicative Subset of C to Safe Rust
by: Fromherz, Aymeric, et al.
Published: (2024)

An Empirical Study of Rust-Specific Bugs in the rustc Compiler
by: Liu, Zixi, et al.
Published: (2025)

Reimplementing Mizar in Rust
by: Carneiro, Mario
Published: (2023)

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
by: Matsushita, Yusuke, et al.
Published: (2026)

Static Deadlock Detection for Rust Programs
by: Zhang, Yu, et al.
Published: (2024)

Suki: Choreographed Distributed Dataflow in Rust
by: Laddad, Shadaj, et al.
Published: (2024)

Filament: Denning-Style Information Flow Control for Rust
by: Ching, Jeffrey C., et al.
Published: (2026)

TYPEPULSE: Detecting Type Confusion Bugs in Rust Programs
by: Chen, Hung-Mao, et al.
Published: (2025)

Translating Large-Scale C Repositories to Idiomatic Rust
by: Dehghan, Saman, et al.
Published: (2025)

Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
by: Lian, Qihao, et al.
Published: (2025)

RustSFQ: A Domain-Specific Language for SFQ Circuit Design
by: Oishi, Mebuki, et al.
Published: (2025)

Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
by: Ho, Son, et al.
Published: (2024)

Characterizing Unsafe Code Encapsulation In Real-world Rust Systems
by: Rao, Zihao, et al.
Published: (2024)

Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring
by: Jacobs, Bart
Published: (2026)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
by: Grannan, Zachary, et al.
Published: (2025)

RustyDL: A Program Logic for Rust
by: Drodt, Daniel, et al.
Published: (2026)

Decompiling Rust: An Empirical Study of Compiler Optimizations and Reverse Engineering Challenges
by: Zhou, Zixu
Published: (2025)

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
by: Britton, Matthew, et al.
Published: (2026)

Raw Pointer Rewriting with LLMs for Translating C to Safer Rust
by: Gao, Yifei, et al.
Published: (2025)

Translating C To Rust: Lessons from a User Study
by: Li, Ruishi, et al.
Published: (2024)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
by: Poli, Federico, et al.
Published: (2024)

Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs
by: Zhang, Kaiwen, et al.
Published: (2022)