达坦科技专注于打造新一代开源跨云存储平台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
