RustHorn: CHC-based Verification for Rust Programs

• DOI: 10.26226/morressier.604907f41a80aac83ca25d55
• Publication Date: 2021-03-23T13:50:22Z
• Authors: Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi
• Keywords: Rust (programming language)

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.