Important references for learning the dark side of operating system development.
Below resources are sorted by my own learning steps, which I found might be efficient.
- MIT 6.887, Formal Reasoning About Programs: https://frap.csail.mit.edu/main
- CMU 15-818A3, Introduction to Separation Logic: https://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2011/cs818A3-11.html
- Software Foundations: https://softwarefoundations.cis.upenn.edu/current/index.html
- Hoare Logic (A chapter of Software Foundations): https://softwarefoundations.cis.upenn.edu/current/Hoare.html
- Separation Logic: A Logic for Shared Mutable Data Structures: https://www.cs.cmu.edu/~jcr/seplogic.pdf
- A Brief Introduction to Separation Logic: https://cs.colorado.edu/~frohardt/SepLogic.pdf
- A Primer on Separation Logic: http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf
- Resources, Concurrency and Local Reasoning: http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf
- Certikos: http://flint.cs.yale.edu/certikos/
- Certiucos: http://staff.ustc.edu.cn/~fuming/research/certiucos/
- Gödel's Incompleteness Theorems: https://plato.stanford.edu/entries/goedel-incompleteness/