利用符號語義進行 Rust 的聲音借用檢查 ( 較長版本 ) Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)

https://arxiv.org/abs/2404.02680

這項工作在理論上為 Rust 的語義提供了新的基礎性貢獻,證明了 LLBC 對於傳統執行模型的正確觀點,並確保其符號語義作為 LLBC 的部分借用檢查器。為證明這些結果,引入了一個新的證明風格,並介紹了名為 join operation 的 LLBC 符號語義的新補充。

via cs.PL updates on arXiv.org

July 2, 2024 at 04:37PM

發佈留言

發佈留言必須填寫的電子郵件地址不會公開。 必填欄位標示為 *