Completed
Translation into Isabelle/Simpl
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Rustv: Semi-automatic Verification of Unsafe Rust Programs
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 This work
- 3 Outline • Overview
- 4 Background
- 5 What we want to do
- 6 The architecture of sel4 verification Verification using theorem prover
- 7 Our approach (in the future) Adapt sel 4's approach to Rust
- 8 Translation into Isabelle/Simpl
- 9 Global heap representation
- 10 Function state space representation
- 11 Example of Verification
- 12 Program translation
- 13 Formalizing safety conditions
- 14 Proof of safety
- 15 Verification Effort
- 16 Interesting example
- 17 Why?
- 18 Some observations
- 19 Future work
- 20 Summary
