Name
Abstract | ||
|---|---|---|
AbstractReduction 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3462205 | ACM Transactions on Programming Languages and Systems |
Keywords | DocType | Volume |
Rust, permission, ownership, pointer, CHC, automated verification | Journal | 43 |
Issue | ISSN | Citations |
4 | 0164-0925 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yusuke Matsushita | 1 | 1 | 0.70 |
| Takeshi Tsukada | 2 | 0 | 2.03 |
| Naoki Kobayashi | 3 | 0 | 3.38 |