论文标题
Rusthorn：基于CHC的RUST程序验证（完整版）
RustHorn: CHC-based Verification for Rust Programs (full version)
论文作者
论文摘要
减少了受约束角条款（CHC）的满足性问题是一种广泛研究的自动化程序验证方法。但是，当前用于指针操作程序的基于CHC的方法不是很可扩展的。本文提出了将指针操作的生锈程序转化为CHC的新颖翻译，该计划通过利用所有权来消除指针和记忆。我们将翻译正式化，以简化生锈的核心并证明其正确性。我们已经为生锈子集实施了原型验证器，并确认了我们方法的有效性。
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
