le-verification

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.

Useful courses

• 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

Automatic therom prover and the basics of proving software (Coq)

• Software Foundations: https://softwarefoundations.cis.upenn.edu/current/index.html

Hoare Logic

• Hoare Logic (A chapter of Software Foundations): https://softwarefoundations.cis.upenn.edu/current/Hoare.html

Separation Logic

• 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

Concurrent Separation Logic

• Resources, Concurrency and Local Reasoning: http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf

Practical OS proofs

• Certikos: http://flint.cs.yale.edu/certikos/
• Certiucos: http://staff.ustc.edu.cn/~fuming/research/certiucos/

Deeper theories

• Gödel's Incompleteness Theorems: https://plato.stanford.edu/entries/goedel-incompleteness/