Concurrent Low-Level System Code Verification

Concurrent program reasoning is hard. There has been many program logics proposed, and they either require special expertise or not reusable systems for arbitrary data structures. Our concern is to come with type assertions which are simple and expressing important properties such as safe heap manipulation in the highly concurrent setting.

Verified Operating System (OS) Abstractions

OS is an important and complex component of the computing stack. We are not only concerned with verification as a reliability task but also rethinking proper abstractions for OS components. Within this context, we investigate modalities for expressing properties of OS components including

  • copy on write file systems
  • virtual memory managers