2 papers
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…
cs.PL2025
End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
Jinhua Wu, Yuting Wang, Liukun Yu +1
Program safety (i.e., absence of undefined behaviors) is critical for correct operation of computer systems. It is usually verified at the source level (e.g., by separation logics)…