Towards Veried Virtual Memory in L4

2004.

Cited by: 19|Views15

Abstract:

We report on the initial stage of an on-going verication project: the formalisation and verication of the L4 -kernel. We describe an abstract model of the virtual memory subsystem in L4, prove safety properties about this model, and describe renemen t of the abstract model towards the implementation of L4. All formalisations and proofs ha...More

Code:

Data:

Get fulltext within 24h
Bibtex
Your rating :
0

 

Tags
Comments