RustHorn: CHC-based Verification for Rust Programs
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Abstract
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.
Topics & Concepts
Computer scienceSoundnessRust (programming language)Pointer (user interface)Programming languageReduction (mathematics)Horn clauseCompleteness (order theory)SatisfiabilityTheoretical computer scienceParallel computingComputer hardwarePrologMathematicsGeometryMathematical analysisFormal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques