Cover Image

Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ho, Son, Fromherz, Aymeric, Protzenko, Jonathan
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
by: Monat, Raphaël, et al.
Published: (2024)

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

CUTECat: Concolic Execution for Computational Law
by: Goutagny, Pierre, et al.
Published: (2024)

On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
by: Enea, Constantin, et al.
Published: (2026)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
by: Grannan, Zachary, et al.
Published: (2025)

Handling Scope Checks (Extended Version)
by: Lee, Michael, et al.
Published: (2026)

Software Model Checking via Summary-Guided Search (Extended Version)
by: Fang, Ruijie, et al.
Published: (2025)

Practical Type-Based Taint Checking and Inference (Extended Version)
by: Karimipour, Nima, et al.
Published: (2025)

Open-World Assertion Checking for Smart Contracts via Game Semantics
by: Koutavas, Vasileios, et al.
Published: (2025)

Law and Order for Typestate with Borrowing
by: Saffrich, Hannes, et al.
Published: (2024)

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

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
by: Wu, Jinhua, et al.
Published: (2026)

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

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

Compositional Symbolic Execution for the Next 700 Memory Models (Extended Version)
by: Lööw, Andreas, et al.
Published: (2025)

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

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

Linearization via Rewriting (Long Version)
by: Lago, Ugo Dal, et al.
Published: (2025)

Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version
by: Karmios, Nat, et al.
Published: (2026)

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

Compilation Semantics for a Programming Language with Versions
by: Tanabe, Yudai, et al.
Published: (2023)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
by: Ling, Hongyi, et al.
Published: (2026)

Conformance Checking for Less: Efficient Conformance Checking for Long Event Sequences
by: Bogdanov, Eli, et al.
Published: (2025)

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

Incremental Proof Development in Dafny with Module-Based Induction
by: Ho, Son, et al.
Published: (2024)

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

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

Borrowing Dirty Qubits in Quantum Programs
by: Su, Bonan, et al.
Published: (2025)

Symbolic Execution Meets Multi-LLM Orchestration: Detecting Memory Vulnerabilities in Incomplete Rust CVE Snippets
by: Abdelrazek, Zeyad, et al.
Published: (2026)

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

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

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

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

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
by: Lööw, Andreas, et al.
Published: (2024)

Teaching LLMs Program Semantics via Symbolic Execution Traces
by: Bayer, Jonas, et al.
Published: (2026)

Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
by: Yao, Yue, et al.
Published: (2024)

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