Verifying the L4 Virtual Memory Subsystem

2004.

Cited by: 21|Views16

Abstract:

We describe aspects of the formalisation and verification of the L4 µ-kernel. Starting from an abstract model of the virtual memory subsystem in L4, we prove safety properties about this model, and then refine the page table abstraction, one part of the model, towards C source code. All formalisations and proofs have been carried out in t...More

Code:

Data:

Get fulltext within 24h
Bibtex
Your rating :
0

 

Tags
Comments