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.
Notes related to Rust language
Magic wand, MIR interpreter (miri), MIR, Ownership types, Prusti verifier, Rust unsafe code, RustBelt verifier, Viper verifier
Papers related to Rust language
- Learning Rust: How experienced programmers leverage resources to learn a new programming language [abtahi:chi:2020]
- Fidelius Charm: Isolating unsafe Rust code [almohri:codaspy:2018]
- Engineering the Servo web browser engine using Rust [anderson:icse:2016]
- Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
- How do programmers use unsafe Rust? [astrauskas:oopsla:2020]
- The meaning of memory safety [azevedo:post:2018]
- System programming in Rust: Beyond safety [balasubramanium:hotos:2017]
- Verifying Rust programs with SMACK [baranowski:atva:2018]
- Verifying safe clients of unsafe code and trait implementations in Rust [beckmann:msc:2020]
- You can't spell trust without Rust [beingessner:msc:2015]
- Theseus: A state spill-free operating system [boos:plos:2017]
- Ownership types for flexible alias protection [clarke:oopsla:1998]
- Deductive program verification for a language with a Rust-like typing discipline type [Internship report] [denis:hal:2020]
- Is Rust used safely by software developers? [evans:icse:2020]
- Extended support for borrowing and lifetimes in Prusti [gorse:msc:2020]
- Safe systems programming in Rust: The promise and the challenge [jung:cacm:2021]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- Stacked borrows: An aliasing model for Rust [jung:popl:2020]
- The Rust programming language [klabnik:book:2018]
- The case for writing a kernel in Rust [levy:apsys:2017]
- Ownership is theft: Experiences building an embedded OS in Rust [levy:plos:2015]
- Multiprogramming a 64kB computer safely and efficiently [levy:sosp:2017]
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
- Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]
- Securing unsafe Rust programs with XRust [liu:icse:2020]
- The Rust language [matsakis:hilt:2014]
- RustHorn: CHC-based verification for Rust programs [matsushita:esop:2020]
- RedLeaf: Towards an operating system for safe and verified firmware [narayanan:hotos:2019]
- Exploiting mixed binaries [papaevripides:acmtps:2021]
- Understanding memory and thread safety practices and issues in real-world Rust programs [qin:pldi:2020]
- Towards making formal methods normal: meeting developers where they are [reid:hatra:2020]
- Rudra: Finding memory safety bugs in Rust at the Ecosystem scale [rudra:sosp:2021]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- Simple verification of Rust programs via functional purification [ullrich:msc:2016]
- KRust: A formal executable semantics of Rust [wang:tase:2018]
- Rust distilled: An expressive tower of languages [weiss:arxiv:2018]
- Memory-safety challenge considered solved? An in-depth study with all Rust CVEs [xu:arxiv:2021]
- GhostCell: Separating permissions from data in Rust [yanovski:unknown:2021]
- VRLifeTime - An IDE tool to avoid concurrency and memory bugs in Rust [zhang:ccs:2020]