MIR

[Google Scholar]

Notes: Rust language, MIR interpreter, undefined behaviour
Papers: jung:popl:2020

MIR is the Rust language’s mid-level intermediate representation.

It has an interpreter miri that attempts to check many kinds of undefined behaviour that is partly described in jung:popl:2020.

RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
Stacked borrows: An aliasing model for Rust [jung:popl:2020]
RustHorn: CHC-based verification for Rust programs [matsushita:esop:2020]

Notes related to MIR