RustHorn: CHC-Based Verification for Rust Programs
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Abstract
Abstract Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
Topics & Concepts
Rust (programming language)Computer scienceProgramming languageTranslation (biology)Core (optical fiber)Horn clauseSoftware engineeringAlgorithmTheoretical computer scienceArtificial intelligenceJavaCorrectnessNatural language processingFormal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques