60 F.Xu et al. in Coq [1].To our knowledge,it is the first verification of (key modules of)a preemptive OS kernel with machine-checkable proofs.The key contribution of the work is to adapt existing theories on interrupt verification [11]and contex- tual refinement of concurrent programs [17,19,24,25],and integrate them into a framework for real-world preemptive OS kernel verification.Specifically,our work makes the following new contributions: First,we formulate and verify the correctness of the APIs of OS ker- nels as contertual refinement between their implementations and specifications. Although refinement approaches have been applied in earlier work on OS kernel verification [4,13,16],we believe our work is the first to explicitly specify and prove contextual refinement for APIs of a preemptive OS kernel,following recent progress on refinement verification of concurrent programs [17,19,24,25].As we explain in Sect.2.2,contextual refinement not only serves as a very strong notion of functional correctness of system APIs,but also allows us to prove properties based on the more abstract API specifications and then carry it down to the level of concrete implementations,which makes the verification much simpler than doing proofs directly at the concrete level. Second,we provide a simple modeling language for specifying kernel prim- itives.The language strives for balance between abstraction and expressiveness for scheduling.On the one hand,we want the specification to abstract away implementation details.On the other hand,it should provide enough details so that many important properties can be specified at the abstract specification level.Our modeling language provides an abstract sched command,allowing us to specify explicitly when the scheduler is invoked in synchronization primi- tives or interrupt handlers.Semantics of sched is parameterized over abstract scheduling policies (e.g.,priority-based or round-robin).Expressiveness about these details are necessary to specify system-wide scheduling properties. Third,we propose a program logic for refinement verification of concurrent kernel programs.The logic supports multi-level nested hardware interrupts and configurable schedulers.It extends concurrent separation logic [21](CSL)with relational assertions that relate program states at the implementation and the specification levels,as in Liang et al.[17,19.It also assigns ownership-transfer semantics to interrupt management operations and verify multi-level hardware interrupts in a realistic setting.Different from traditional Hoare-style program logics,whose soundness ensures the semantic interpretation of Hoare-triples, our logic explicitly establishes contextual refinement,which is more useful for establishing abstractions for system APIs,as explained above. Fourth,our framework is developed for a practical subset of C.It has been successfully applied to verify key APIs of uC/OS-II [2],including the timer inter- rupt handler (and a pseudo interrupt handler to demonstrate the support of multi-level interrupts),the scheduler,the time management,and four synchro- nization mechanisms:message queues,mail boxes,semaphores,and mutexes. It is worth noting that,unlike existing works [4,13,16,27]that are focused on kernels newly developed with verification in mind,we take a commercial system developed by an independent third-party and verify the code with minimum mod- ification,which demonstrates the generality and applicability of our framework.60 F. Xu et al. in Coq [1]. To our knowledge, it is the first verification of (key modules of) a preemptive OS kernel with machine-checkable proofs. The key contribution of the work is to adapt existing theories on interrupt verification [11] and contex￾tual refinement of concurrent programs [17,19,24,25], and integrate them into a framework for real-world preemptive OS kernel verification. Specifically, our work makes the following new contributions: First, we formulate and verify the correctness of the APIs of OS ker￾nels as contextual refinement between their implementations and specifications. Although refinement approaches have been applied in earlier work on OS kernel verification [4,13,16], we believe our work is the first to explicitly specify and prove contextual refinement for APIs of a preemptive OS kernel, following recent progress on refinement verification of concurrent programs [17,19,24,25]. As we explain in Sect. 2.2, contextual refinement not only serves as a very strong notion of functional correctness of system APIs, but also allows us to prove properties based on the more abstract API specifications and then carry it down to the level of concrete implementations, which makes the verification much simpler than doing proofs directly at the concrete level. Second, we provide a simple modeling language for specifying kernel prim￾itives. The language strives for balance between abstraction and expressiveness for scheduling. On the one hand, we want the specification to abstract away implementation details. On the other hand, it should provide enough details so that many important properties can be specified at the abstract specification level. Our modeling language provides an abstract sched command, allowing us to specify explicitly when the scheduler is invoked in synchronization primi￾tives or interrupt handlers. Semantics of sched is parameterized over abstract scheduling policies (e.g., priority-based or round-robin). Expressiveness about these details are necessary to specify system-wide scheduling properties. Third, we propose a program logic for refinement verification of concurrent kernel programs. The logic supports multi-level nested hardware interrupts and configurable schedulers. It extends concurrent separation logic [21] (CSL) with relational assertions that relate program states at the implementation and the specification levels, as in Liang et al. [17,19]. It also assigns ownership-transfer semantics to interrupt management operations and verify multi-level hardware interrupts in a realistic setting. Different from traditional Hoare-style program logics, whose soundness ensures the semantic interpretation of Hoare-triples, our logic explicitly establishes contextual refinement, which is more useful for establishing abstractions for system APIs, as explained above. Fourth, our framework is developed for a practical subset of C. It has been successfully applied to verify key APIs of μC/OS-II [2], including the timer inter￾rupt handler (and a pseudo interrupt handler to demonstrate the support of multi-level interrupts), the scheduler, the time management, and four synchro￾nization mechanisms: message queues, mail boxes, semaphores, and mutexes. It is worth noting that, unlike existing works [4,13,16,27] that are focused on kernels newly developed with verification in mind, we take a commercial system developed by an independent third-party and verify the code with minimum mod￾ification, which demonstrates the generality and applicability of our framework