Challenges of concurrent Kerne|∨ erification Verifying concurrent programs is difficult Non-deterministic interleaving Verifying concurrent kernel is more challenging OS verification is usually based on refinement verification Concurrent kernel verification requires combination of verifying refinement and concurrency Difficult to do it compositionally Theoretical problems have not been solved until recently [Liang et al. PLDI13, LICS 14][Turon et al. POPL13, ICFP 13 Concurrency caused by preemptions and multi-level interrupts are avoided by previous Os verification projects e.g. seL4 [Klein et al. SOSP 09, CertiKos [Gu et al. POPL' 15]Challenges of Concurrent Kernel Verification • Verifying concurrent programs is difficult – Non-deterministic interleaving • Verifying concurrent kernel is more challenging – OS verification is usually based on refinement verification – Concurrent kernel verification requires combination of verifying refinement and concurrency • Difficult to do it compositionally • Theoretical problems have not been solved until recently [Liang et al. PLDI’13, LICS’14] [Turon et al. POPL’13, ICFP’13] Concurrency caused by preemptions and multi-level interrupts are avoided by previous OS verification projects e.g. seL4 [Klein et al. SOSP‘09], CertiKOS[Gu et al. POPL’15]