RustHorn: CHC-based Verification for Rust Programs
2021 ◽
Vol 43
(4)
◽
pp. 1-54
Keyword(s):
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.
1976 ◽
Vol C-25
(11)
◽
pp. 1101-1109
◽
Keyword(s):
Keyword(s):
Keyword(s):
1991 ◽
Vol 5
(1)
◽
pp. 122-127