Showing cs.PLShow all
3 papers · 1 filter
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)…
cs.PL2023
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)
Ling Zhang, Yuting Wang, Jinhua Wu +2
Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous i…