Formal pervasive verification of a paging mechanism
The work
| Authors | Eyad Alkassar; Norbert Schirmer; Artem Starostin |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2008 |
| Citekey | alkassar2008formal |
Where it appeared
| Published in | International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| Publisher | Springer |
| Pages | 109--123 |
Abstract
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.
A copy is held
pdf, 6.3 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | import via bibtex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-16 15:32 UTC |
Filed under
Cite it as
@inproceedings{alkassar2008formal,
title = {Formal pervasive verification of a paging mechanism},
author = {Eyad Alkassar and Norbert Schirmer and Artem Starostin},
year = {2008},
booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
publisher = {Springer},
pages = {109--123},
}
This record lives at https://refs.drheap.org/alkassar2008formal/ and will keep doing so.