This website requires JavaScript.

Modular Formal Verification of Rust Programs with Unsafe Blocks

Nima Rahimi ForoushaaniBart Jacobs
Dec 2022
摘要
Rust is a modern systems programming language whose type system guaranteesmemory safety. For the sake of expressivity and performance it allowsprogrammers to relax typing rules temporarily, using unsafe code blocks.However, in unsafe blocks, the burden of making sure that the code does not endup having undefined behaviour is on the programmer. Even most expertprogrammers make mistakes and a memory safety bug in an unsafe block rendersall the type system guarantees void. To address this problem we are trying toverify soundness of Rust unsafe code applying our Modular Symbolic Executionalgorithm. This text outlines our approach and the progress that has been madeso far.
展开全部
图表提取

暂无人提供速读十问回答

论文十问由沈向洋博士提出,鼓励大家带着这十个问题去阅读论文,用有用的信息构建认知模型。写出自己的十问回答,还有机会在当前页面展示哦。

Q1论文试图解决什么问题?
Q2这是否是一个新的问题?
Q3这篇文章要验证一个什么科学假设?
0
被引用
笔记
问答