Simple verification of Rust programs via functional purification

Sebastian Ullrich
[Google Scholar] [DBLP] [Citeseer]
Read: 08 May 2020

Masters thesis
Karlsruhe Institut of Technology
2016
Note(s): Rust language, Horn clause
Papers: matsushita:esop:2020, demoura:cade:2015

Transpiles Rust code to a functional program in Lean (demoura:cade:2015) to allow verification of Rust programs in Lean. Demonstrated on a binary search implementation.

The implementation is here.