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.
Notes related to MIR
MIR interpreter (miri), RustBelt verifier
Papers related to MIR
- 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]