Formal pervasive verification of a paging mechanism

Abstract. Memory virtualization by means of demand paging is a crucial com-ponent of every modern operating system. The formal verification is challenging since reasoning about the page fault handler has to cover two concurrent com-putational sources: the processor and the hard disk. We accurately model the in-terleaved executions of devices and the page fault handler, which is written in a high-level programming language with inline assembler portions. We describe how to combine results from sequential Hoare logic style reasoning about the page fault handler on the low-level concurrent machine model. To the best of our knowledge this is the first example of pervasive formal verification of software communicating with devices.