Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool for Rust. RustyDL reasons about Rust programs directly on the source code level, in contrast to other tools that are all based on translation to an intermediate language. A source-level program logic for Rust is crucial for a human-in-the-loop (HIL) style of verification that permits proving highly complex functional properties. We discuss specific Rust challenges in designing a program logic and calculus for HIL-style verification and propose a solution in each case. We provide a proof-of-concept of our ideas in the form of a prototype of a Rust instance of the deductive verification tool KeY.

翻译：Rust 是一种现代编程语言，它通过强大的类型系统保证了内存安全性和数据竞争的不存在。我们提出了 RustyDL，一种适用于 Rust 的程序逻辑，作为 Rust 自动交互式演绎验证工具的基础。与其他所有基于翻译到中间语言的工具不同，RustyDL 直接在源代码级别对 Rust 程序进行推理。对于 Rust 而言，一个源代码级别的程序逻辑对于实现人在回路（HIL）风格的验证至关重要，这种验证方式允许证明高度复杂的功能属性。我们讨论了为 HIL 风格验证设计程序逻辑和演算时所面临的特定 Rust 挑战，并在每种情况下提出了解决方案。我们以演绎验证工具 KeY 的 Rust 实例原型的形式，提供了我们这些想法的概念验证。