Rust language

Rust language
[Google Scholar] [Wikipedia]

Notes: ownership types, Prusti verifier, SMACK verifier, Regions
Papers: anderson:icse:2016, astrauskas:oopsla:2019, baranowski:atva:2018, jung:popl:2017, jung:popl:2020, levy:apsys:2017, toman:ase:2015

Rust is a systems programming language that differs from C in that it aims for high performance without sacrificing memory safety. It achieves this using an unusual ownership type system that largely eliminates aliasing problems and simplifies the creation of concurrent programs.

Verifiers for Rust include Prusti verifier, SMACK verifier

An incredibly early description of Rust is here but many aspects of the language have changed since 2010.

Magic wand, MIR interpreter (miri), MIR, Ownership types, Prusti verifier, Rust unsafe code, RustBelt verifier, Viper verifier