Creusot: A Foundry for the Deductive Verification of Rust Programs
Creusot: A Foundry for the Deductive Verification of Rust Programs
复制标题
Creusot：Rust 程序演绎验证的铸造厂
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
C. Marché
中科院分区：
文献类型：
--
作者：
Xavier Denis;Jacques;C. Marché
． Rust是一种相对较新的系统编程语言，它通过严格的所有权策略提供内存安全的静态保证。该特性带来的强大保证为演绎验证（cid:28）验证打开了有希望的进展，其目的是证明Rust代码在其预期行为的规范（cid:28）验证方面的一致性。我们介绍了Creusot的基础，这是一个用于Rust代码的形式规范（cid:28）和演绎验证（cid:28）验证的工具。（cid:28）第一个原创性来自Creusot的spec （cid:28）语言，其特点是预言的概念来推理记忆突变，与Rust的所有权系统协调工作。第二个创新是Creusot如何在Rust trait系统的基础上构建，以提供几个高级抽象特性。
. Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strict ownership policy. The strong guarantees brought by this feature opens promising progress for deductive veri(cid:28)cation , which aims at proving the conformity of Rust code with respect to a speci(cid:28)cation of its intended behavior. We present the foundations of Creusot , a tool for the formal speci(cid:28)cation and deductive veri(cid:28)cation of Rust code. A (cid:28)rst originality comes from Creusot ’s speci(cid:28)cation language, which features a notion of prophecy to reason about memory mutation, working in harmony with Rust’s ownership system. A second originality is how Creusot builds upon Rust trait system to provide several advanced abstraction features.