Compositional Development of Certified System Software

on YouTube ↗49m

" summary

Claims a new semantics that makes horizontal and vertical composition of linearizable concurrent objects workable, replacing ad hoc inlining with a categorical fix: use the Karoubi envelope to absorb emergent behaviors from the composition identity and define saturation (K-construction) so a concurrent object plus a concurrent copycat yields a compositional spec. Implements this in the CertiKOS ecosystem (verified kernels with 37 abstraction layers, ~3k LOC base, ComperX-based compilation), proves contextual refinement and locality without relying on atomicity or happens‑before.

AI-written summary · about

" chapters (14)

1. 0:00Certified system software intro
2. 0:45OS formal verification challenges
3. 3:51Need for compositional verification
4. 6:20DeepSpec project methodology
5. 8:48Deep specifications for compositionality
6. 11:41Limitations of verification tools
7. 15:35Linearizability as composition theory
8. 20:32Beyond atomicity in linearizability
9. 24:25Horizontal and vertical composition
10. 31:27Sequentially consistent games
11. 35:04Abstract linearizability and trace equivalence
12. 39:00Contextual refinement and locality
13. 41:12Future directions in verification
14. 43:24Q&A