Cover Image

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wu, Jinhua, Wang, Yuting, Yu, Liukun, Meng, Linglong
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

Crux, a Precise Verifier for Rust and Other Languages
by: Pernsteiner, Stuart, et al.
Published: (2024)

Scylla: Translating an Applicative Subset of C to Safe Rust
by: Fromherz, Aymeric, et al.
Published: (2024)

An Empirical Study of Rust-Specific Bugs in the rustc Compiler
by: Liu, Zixi, et al.
Published: (2025)

VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners
by: Yang, Aidan Z. H., et al.
Published: (2024)

Lessons Learned So Far From a Community Effort to Verify the Rust Standard Library (work-in-progress)
by: Blanc, Alex Le, et al.
Published: (2025)

PermRust: A Token-based Permission System for Rust
by: Gehring, Lukas, et al.
Published: (2025)

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions
by: Tas, Wannes, et al.
Published: (2026)

NPB-Rust: NAS Parallel Benchmarks in Rust
by: Martins, Eduardo M., et al.
Published: (2025)

Decompiling Rust: An Empirical Study of Compiler Optimizations and Reverse Engineering Challenges
by: Zhou, Zixu
Published: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
by: Jamner, Dustin, et al.
Published: (2025)

RustMC: Extending the GenMC stateless model checker to Rust
by: Pearce, Oliver, et al.
Published: (2025)

Auditing Rust Crates Effectively
by: Zoghbi, Lydia, et al.
Published: (2026)

Charon: An Analysis Framework for Rust
by: Ho, Son, et al.
Published: (2024)

Surveying the Rust Verification Landscape
by: Blanc, Alex Le, et al.
Published: (2024)

A Verified Compiler for Quantum Simulation
by: Li, Liyi, et al.
Published: (2025)

Annotating and Auditing the Safety Properties of Unsafe Rust
by: Rao, Zihao, et al.
Published: (2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
by: Rinard, Martin
Published: (2026)

Static Deadlock Detection for Rust Programs
by: Zhang, Yu, et al.
Published: (2024)

Cocoon: Static Information Flow Control in Rust
by: Lamba, Ada, et al.
Published: (2023)

A Hybrid Approach to Semi-automated Rust Verification
by: Ayoun, Sacha-Élie, et al.
Published: (2024)

Verifying Sequential Consistency under Bounded Preemptions
by: Govind, R., et al.
Published: (2026)

An Interactive Debugger for Rust Trait Errors
by: Gray, Gavin, et al.
Published: (2025)

Garbage Collection for Rust: The Finalizer Frontier
by: Hughes, Jacob, et al.
Published: (2025)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Translating Large-Scale C Repositories to Idiomatic Rust
by: Dehghan, Saman, et al.
Published: (2025)

&inator: Correct, Precise C-to-Rust Interface Translation
by: Chen, Victor, et al.
Published: (2026)

Verifying Peephole Rewriting In SSA Compiler IRs
by: Bhat, Siddharth, et al.
Published: (2024)

Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
by: Lian, Qihao, et al.
Published: (2025)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
by: Tekriwal, Mohit, et al.
Published: (2025)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
by: Paraskevopoulou, Zoe
Published: (2026)

Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations (Extended Version)
by: Qiu, Jie, et al.
Published: (2024)

TYPEPULSE: Detecting Type Confusion Bugs in Rust Programs
by: Chen, Hung-Mao, et al.
Published: (2025)

Towards a Transpiler for C/C++ to Safer Rust
by: Tripuramallu, Dhiren, et al.
Published: (2024)

Reimplementing Mizar in Rust
by: Carneiro, Mario
Published: (2023)

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
by: Matsushita, Yusuke, et al.
Published: (2026)

RustSFQ: A Domain-Specific Language for SFQ Circuit Design
by: Oishi, Mebuki, et al.
Published: (2025)

Suki: Choreographed Distributed Dataflow in Rust
by: Laddad, Shadaj, et al.
Published: (2024)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
by: Gross, Jason, et al.
Published: (2022)