Formal Refinement for Operating System Kernels

This book was written as a companion to my book on modelling operating system kernels. The second kernel, the Separation Kernel, is new and was partly constructed out of the kit of parts (and the reader will see reuse in its speci?cation and re?nement) and was included for speci?c reasons that will become clear anon.