A certified page allocator in uCore

Date:

An introduction to verified microkernels, Serval verification framework, and our work.