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}
}