Operating Systems Kernels

In the recently started and still ongoing research reported here, the ASM (Abstract State Machines) method is used as a practically viable method for defining, in a rigorous but concise way, satisfactory models for OS kernels and to prove properties of interest for them. A main goal is to make these models refinable in a controllable way to executable code.