Presented as part of the 2016 HCSS conference.
ABSTRACT
Existing modelled and veried operating systems (OS's) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential.
