10 citations · 10 across the 3 of their papers we have counts for
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★ 10 cited
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…