| 1 |
Wed |
Jan 22 |
Administrivia, introduction to TLA+ (slides) |
Ch 1-4 of Specifying Systems (L. Lamport) |
| 2 |
Mon |
Jan 27 |
Liveness, Instantiation (slides) |
Ch 8 of Specifying Systems (L. Lamport) |
| 2 |
Wed |
Jan 29 |
Introduction to Dafny (slides) |
Dafny tutorial |
| 3 |
Mon |
Feb 3 |
Refinement (slides) |
Section 10.8 of Specifying Systems |
| 3 |
Wed |
Feb 5 |
Review |
|
| 4 |
Mon |
Feb 10 |
Certikos (Yunhao) |
paper |
| 4 |
Wed |
Feb 12 |
Implementing TLS with Verified Cryptographic Security (Daniel M.) |
paper |
| 5 |
Mon |
Feb 17 |
Memory and Concurrent Access (slides) |
Ch 5 of Specifying Systems |
| 5 |
Wed |
Feb 19 |
Kleene Algebras and NetKat (Cosmo) |
paper |
| 6 |
Mon |
Feb 24 |
break |
|
| 6 |
Wed |
Feb 26 |
Verifying Programmable Networks (Andy) |
paper |
| 7 |
Mon |
Mar 4 |
Peterson's Algorithm with TLC Model Checker |
demo |
| 7 |
Wed |
Mar 6 |
Q&A with Leslie Lamport |
|
| 8 |
Mon |
Mar 11 |
On Methodologies for Formal Verification of Consensus Protocols (Haobin) |
paper |
| 8 |
Wed |
Mar 13 |
Jasmin: High-assurance and high-speed cryptography (Josh) |
paper |
| 9 |
Mon |
Apr 6 |
Model Checking and TLC (slides) |
Ch 14 of Specifying Systems |
| 9 |
Wed |
Apr 8 |
TLAPS (Daniel W.) |
paper |
| 10 |
Mon |
Apr 13 |
CompCert (Pedro) |
paper |
| 10 |
Wed |
Apr 15 |
SecVerilog |
paper |
| 11 |
Mon |
Apr 20 |
Oded Padon: Ivy (slides) |
paper |
| 11 |
Wed |
Apr 22 |
Real-time and Composition (slides) |
Ch 8, 10 of Specifying Systems |
| 12 |
Mon |
Apr 27 |
Tahina Ramanandro: EverParse (slides) |
paper |
| 12 |
Wed |
Apr 29 |
Manos Kapritsos: IronFleet |
paper |