pintjuk/awesome-theorem-proving

Rerousces and cool papers on theorem proving, formal varification, and logic

Awesome Theorem Proving

A list of awesome papers and cool resources on theorem proving, formal software verification and logic. Don't hesitate to suggest resources in other subfields of transfer learning. I accept pull requests

Table Of Content

• Awesome Theorem Proving
• Table Of Content
• Tutorials
• Papers
  • Concurency
  • OS verifcation

Tutorials

Talk:What's new in the world of seL4? TODO: watch

Papers

Concurency

• A Marriage of Rely/Guarantee and Separation Logic (Vafeiadis 2007)
• The Clustered Multikernel: An Approach toFormal Verification of Multiprocessor OS Kernels (2019)

Survays

• Modular fine-grained concurrency verification (Vafeiadis 2008)

Not technicaly a servay but background is very comprehensive

OS verifcation

• Time Protection: The Missing OS Abstraction (Ge 2019) TODO: read
• The Clustered Multikernel: An Approach toFormal Verification of Multiprocessor OS Kernels (2019) TODO: read!
• seL4: Comprehensive Formal Verification of an OS Microkernel (Klein 2014)
• seL4: seL4: Formal verification of an OS kernel (Klein 2009)

Surays

• Operating system verification—An overview (Klein 2009)

Vision

• Correct, Fast, Maintainable – Choose Any Three! (Blackham 2012)
• What if you could actually Trust your kernel? (Heiser 2011)
• It’s Time for Trustworthy Systems