Reduction to the satisfiability 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 memories 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.

RustHorn: CHC-based Verification for Rust Programs

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme