Deductive program verification for a language with a Rust-like typing discipline

Deductive program verification seeks to eliminate bugs in software by translating programs annotated with specifications into logical formulas which are then solved using semi-automated tools. When verifying programs using a mutable heap, it is often required to show that pointers do not alias each other, ensuring there is only one way to modify structures in memory. This leads to cumbersome proof obligations and makes verification much more challenging. Newer languages like Rust feature pointers as well but prevent aliasing through the type system. This opens the door to simpler approaches to verification, free of tedious proof obligations. We propose a technique for the verification of Rust programs by translation to a functional language. The challenge of this translation is the handling of mutable borrows, pointers with control of aliasing in a region of memory. To overcome this, we used a technique inspired by prophecy variables to predict the final values of borrows. The main contribution of this work is to prove this translation correct. We developed a proof-of-concept tool to show the viability of this approach