One of the challenges in verifying systems level code is the low-level, untyped view of the machine state that operating systems have. We describe a way to faithfully formalise this view while at the same time providing an easy-to-use, abstract and typed view of memory where possible. We have used this formal memory model to verify parts of the virtual memory subsystem of the L4 high-performance microkernel. All formalisations and proofs have been carried out in the theorem prover Isabelle and the verified code has been integrated into the current implementation of L4. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Tuch, H., & Klein, G. (2005). A unified memory model for pointers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 474–488). https://doi.org/10.1007/11591191_33
Mendeley helps you to discover research relevant for your work.