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