10 citations · 10 across the 3 of their papers we have counts for
Showing 2026 · cs.PLShow all
2 papers · 2 filters
cs.PL2026
Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation
Jinhua Wu, Yuting Wang, Zhemin Chen
Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees t…
cs.PL2026
RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
Jinhua Wu, Yuting Wang, Liukun Yu +1
We present our ongoing work on developing an end-to-end verified Rust compiler based on CompCert. It provides two guarantees: one is semantics preservation from Rust to assembly, i…