本文主要从以下2点来进行错误的检测：

• 利用 Rust 编译器在编译时为无法检查的安全条件自动生成的断言，以其为验证条件，检查例如越界访问和整数溢出等问题。
• Unsafe code 破坏所有权系统，导致悬空指针、共享可变别名等问题。

在做开题报告的时候找到了这篇论文，挺巧妙的想法，简单记录一下其思路。

本文详细介绍了动态污点分析（Dynamic Taint Analysis）和前向符号执行（Forward Symbolic Execution）。

本文是对综述论文 Fuzzing: a survey¹, Fuzzing: A Survey for Roadmap² 和 The art, science, and engineering of fuzzing: A survey³ 的归纳总结。

本文提出了 Yggdrasil，Yggdrasil 是一个工具包，可用于编写具有一键验证功能的文件系统。它通过一种称为崩溃细化的新颖正确性定义实现自动化验证，无需手动注释或证明实现代码，并在出现错误时生成反例。崩溃细化适用于完全自动化的 SMT 推理，并使开发人员能够模块化地实现文件系统以进行验证。

这篇论文介绍了一个名为Serval的框架，用于通过符号执行来对系统代码进行可扩展的自动化验证。

Serval的核心思想是将开发人员使用Rosette编写指令集解释器并转化为自动化验证器，从而实现系统软件的验证。这一框架通过符号性能分析和优化来识别和修复验证性能瓶颈。作者通过将Serval应用于现有的系统和未经验证的系统中，展示了其在找到系统错误和提高验证效率方面的有效性。