Undefined behaviour

[Google Scholar] [Wikipedia]

Notes: Frama-C verifier, Rust unsafe code
Papers: wang:sosp:2013

Undefined behaviour is program behaviour that is not defined by the programming language or by its implementation making the behaviour of the program unpredictable and sensitive to the compiler version and optimiziation flags wang:sosp:2013.

Frama-C verifier, Memory safety, MIR interpreter (miri), MIR, Rust unsafe code, RustBelt verifier