RustHorn: CHC-based verification for Rust programs

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 06 May 2020

Programming Languages and Systems
Springer International Publishing
Cham
Pages 484-514
2020
Note(s): Rust language, MIR, Horn clause
Papers: gurfinkel:cav:2015, astrauskas:oopsla:2019, baranowski:atva:2018, ullrich:msc:2016

Verifies Rust programs by converting basic blocks in the MIR representation of the code into Constrained Horn Clauses (CHCs) that are then verified using Horn clause support in Z3 or HoIce.

The conversion reminds me of Electrolysis (that translates Rust to Lean functions) while the use of Horn clauses reminds me of SeaHorn (that translates LLVM IR to Horn clauses).

The implementation is here.

  • Simple verification of Rust programs via functional purification [ullrich:msc:2016]