Operating systems

[Google Scholar] [Wikipedia]


NOVA hypervisor, Serval solver-based verifier

  • A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
  • Theseus: A state spill-free operating system [boos:plos:2017]
  • Using continuations to implement thread management and communication in operating systems [draves:sosp:1991]
  • Aspect weaving as component knitting: Separating concerns with Knit [eide:aspse:2001]
  • Static and dynamic structure in design patterns [eide:icse:2002]
  • SeL4: Formal verification of an OS kernel [klein:sosp:2009]
  • On the duality of operating system structures [lauer:osr:1979]
  • The case for writing a kernel in Rust [levy:apsys:2017]
  • Ownership is theft: Experiences building an embedded OS in Rust [levy:plos:2015]
  • Multiprogramming a 64kB computer safely and efficiently [levy:sosp:2017]
  • A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
  • Formally verified memory protection for a commodity multiprocessor hypervisor [li:usenix:2021]
  • Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
  • Lock inference for systems software [regehr:acp4is:2003]
  • Knit: Component composition for systems software [reid:osdi:2000]
  • Translation validation for a verified OS kernel [sewell:pldi:2013]
  • Program verification in the presence of cached address translation [syeda:itp:2018]
  • Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]