RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
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.e., the behaviors of source code includes the behaviors of target code, with which the properties verified at the sourc...
Збережено в:
| Автори: | , , , |
|---|---|
| Формат: | Стаття |
| Опубліковано: |
2026
|
| Предмети: | |
| Онлайн доступ: | https://arxiv.org/abs/2602.07455 http://arxiv.org/abs/2602.07455 |
| Теги: |
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|