Formal Pervasive Verification of a Paging Mechanism

Eyad Alkassar and Norbert Schirmer and Artem Starostin

Paper on TACAS, 2008


Memory virtualization by means of demand paging is a crucial component of every modern operating system. The formal verification is challenging since reasoning about the page fault handler has to cover two concurrent computational sources: the processor and the hard disk. We accurately model the interleaved 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.

 Online Copy

Available as PDF-File

 BibTeX Entry

AUTHOR = {Alkassar, Eyad and Schirmer, Norbert and Starostin, Artem},
TITLE = {Formal Pervasive Verification of a Paging Mechanism},
VOLUME = {4963}, 
YEAR = {2008},
PAGES = {109-123}, 
BOOKTITLE = {14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08)}, 
PUBLISHER = {Springer},
EDITOR = {C. R. Ramakrishnan and Jakob Rehof},
EE = {},

Norbert Schirmer