Rust Verification Workshop 2021

Videos

• 

  1 — Peeking at compiler-internal data (for fun and profit)
• 

  2 — Verifying that Rust programs don't crash
• 

  3 — crux-mir: Symbolic testing for Rust
• 

  4 — Polonius
• 

  5 — Rustv: Semi-automatic Verification of Unsafe Rust Programs
• 

  6 — Towards Automatic Verification of Unsafe Rust with Constrained Horn Solvers
• 

  7 — Rust interest in safety- and mission-critical environments
• 

  8 — Prusti – Deductive Verification for Rust
• 

  9 — Creusot: A prototype tool for verification of Rust software
• 

  10 — hacspec: succinct, executable, verifiable specifications for high-assurance cryptography
• 

  11 — Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
• 

  12 — RustBelt: A Quick Dive Into the Abyss
• 

  13 — Ferrite: A Rust EDSL for Message-passing Protocol Verification