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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Alkassar, E., Schirmer, N., & Starostin, A. (2008). Formal pervasive verification of a paging mechanism. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4963 LNCS, pp. 109–123). https://doi.org/10.1007/978-3-540-78800-3_9
Mendeley helps you to discover research relevant for your work.