一句话：提出将带指针与动态内存的 Rust 程序归约为 CHC 的新方法，利用权限保证消除指针和内存状态，并证明可靠性与完备性。
约束 Horn 子句（CHC）归约是自动程序验证的常用途径，但现有方法难以处理指针操作程序，尤其是涉及动态内存分配者。本文提出一种针对 Rust 程序的新型 CHC 归约：借助 Rust 的权限（ownership 与 borrowing）保证，消除显式指针与内存状态，将程序验证问题转化为 CHC 可满足性。作者在简化的 Rust 核心语言上形式化该归约，并证明其可靠性（soundness）与完备性（completeness）；还实现了面向 Rust 子集的原型验证器，实验确认了方法有效性。
Reduction to satisfiability of constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. Current CHC-based methods, however, do not work very well for pointer-manipulating programs, especially those with dynamic memory allocation. This article presents a novel reduction of pointer-manipulating Rust programs into CHCs, which clears away pointers and memory states by leveraging Rust’s guarantees on permission. We formalize our reduction for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
@article{paperbot1210,
title = {RustHorn: CHC-based Verification for Rust Programs},
author = {Yusuke Matsushita and Takeshi Tsukada and Naoki Kobayashi},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {4},
year = {2021},
doi = {10.1145/3462205}
}