Ownership guided C to Rust translation

DOI10.1007/978-3-031-37709-9_22MaRDI QIDQ6535702zbMATH OpenFDO

Authors Cristina David, Yijun Yu, Meng Wang

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37709-9_22

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• RustHorn: CHC-based verification for Rust programs
• Translating Xd-C programs to MSVL programs
• Convert2Java: semi-automatic conversion of C to Java
• Formally understanding Rust's ownership and borrowing system at the memory level
• Interprocedural and flow-sensitive type analysis for memory and type safety of C code

Cites work

• A semantics for concurrent separation logic
• scientific article; zbMATH DE number 1304000 (Why is no real title available?)
• Implicit ownership types for memory management
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Local rely-guarantee reasoning
• Ownership types for object encapsulation
• Points-to analysis with efficient strong updates
• RustHorn: CHC-based verification for Rust programs
• Variables as resource for shared-memory programs: semantics and soundness
• Viper: a verification infrastructure for permission-based reasoning

This page was built for publication: Ownership guided C to Rust translation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535702)