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