共计 925 个字符，预计需要花费 3 分钟才能阅读完成。
达坦科技专一于打造新一代开源跨云存储平台 DatenLord，通过软硬件深度交融的形式买通云云壁垒，致力于解决多云架构、多数据中心场景下异构存储、数据对立治理需要等问题，以满足不同行业客户对海量数据跨云、跨数据中心高性能拜访的需要。在本周的前沿技术分享中，咱们邀请到了 王俊吉，来为大家分享RustBelt 与 Rust 形式化办法。
01、演讲题目
RustBelt 与 Rust 形式化办法
02、演讲工夫
2023 年 9 月 3 日上午 10:30
03、演讲人
王俊吉
Rust 编译器 / 形式化办法爱好者。
04、引言
RustBelt 是 Rust 语言内存平安的形式化语义模型，将比照与其余 Rust 形式化验证工具的差别，并选取 RustBelt 中所有权的局部作简要介绍。
05、内容简介
Rust 是一门内存平安的零碎编程语言，通过所有权、生命周期标注等伎俩在编译期实现内存平安。同时，Rust 也提供了隔离的 unsafe 机制，容许绕过局部安全检查以实现更精密的内存拜访等需要。在 Rust 规范库中，存在大量的 unsafe 代码，其内存安全性存疑。基于此背景下，RustBelt 我的项目提出了可用于证实 Rust 代码内存安全性的语义模型，将 Rust MIR 代码经简化后手工转写为 λ -Rust 的形式化语言后，RustBelt 语义模型保障只有能通过 λ -Rust 的类型查看，则该段代码是内存平安的。
06、直播预约
欢迎您预约直播，或者登陆腾讯会议观看直播：
会议号：474-6575-9473
达坦科技（DatenLord）专一下一代云计算——“天空计算”的基础设施技术，致力于拓宽云计算的边界。达坦科技打造的新一代开源跨云存储平台 DatenLord，通过软硬件深度交融的形式买通云间壁垒，实现数据高效跨云拜访，建设海量异地、异构数据的对立存储拜访机制，为云上利用提供高性能平安存储反对。以满足不同行业客户对海量数据跨云、跨数据中心高性能拜访的需要。
公众号 ：达坦科技 DatenLord
DatenLord 官网：http://www.datenlord.io
知乎账号：
https://www.zhihu.com/org/da-tan-ke-ji
B 站：
https://space.bilibili.com/2017027518