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.
Notes related to Undefined behaviour
Frama-C verifier, Memory safety, MIR interpreter (miri), MIR, Rust unsafe code, RustBelt verifier
Papers related to Undefined behaviour
- Don't look UB: Exposing sanitizer-eliding compiler optimizations [isemann:pldi:2023]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- Stacked borrows: An aliasing model for Rust [jung:popl:2020]
- SoK: Eternal war in memory [szekeres:sandp:2013]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- Towards optimization-safe systems: Analyzing the impact of undefined behavior [wang:sosp:2013]