1.
Syllabus
❱
1.1.
Administrative Information
1.2.
Course Schedule
1.3.
Class Prep
1.4.
Programming Assignments
1.5.
Course Project
1.6.
Paper Discussion
1.7.
Approval Instructions
2.
Week 1: Rust
❱
2.1.
System Setup
2.2.
Basic Syntax of Rust
2.3.
Safety Features of Rust
2.4.
Expressive Power and Unsafe Rust
2.5.
More on Struct and Traits
3.
Week 2: Rust (Continued)
❱
3.1.
Lifetimes
3.2.
?, dyn, and Macros
3.3.
Useful Crates and Tools
3.4.
Idioms and Design Patterns
❱
3.4.1.
Use Expressions
3.4.2.
Use Pattern Matching and Destructuring
3.4.3.
Use Iterators
3.4.4.
Avoid Declaring First
3.4.5.
Think About clone() Before Using It
3.4.6.
Use the Debug Formatter
3.4.7.
Use #[derive()]
3.4.8.
Implement the Display Trait
3.4.9.
Implement new()
3.4.10.
Implement the Default Trait Along with new()
3.4.11.
match De-Nesting
3.4.12.
Processing Collections of Items Using Functional Language Features
3.4.13.
Use Method Chaining
3.4.14.
Error Handling
3.4.15.
New Type Idiom
3.4.16.
Use &str, &T, and &[T] for Function Parameters
4.
Week 3: Fuzz Testing, Property-Based Testing, Symbolic Execution, and SAT/SMT
5.
Week 5: Rust analyses
6.
Week 6: Rust OSes
7.
Week 7: Symbolic Execution
8.
Week 8: Hybrid Fuzzing
9.
Week 9: Formal Methods
10.
Week 10: Formal Methods (Continued)
11.
Week 11: Interactive Verification
12.
Week 12: Automated Verification
Light (default)
Rust
Coal
Navy
Ayu
CMPT 479/982
Week 12: Automated Verification
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
A Formally Verified NAT
Hyperkernel: Push-Button Verification of an OS Kernel
Ironclad Apps: End-to-End Security via Automated Full-System Verification