@inproceedings{TuchKleinOSV04,
  author = 	 {Harvey Tuch and Gerwin Klein},
  title = 	 {Verifying the {L4} Virtual Memory Subsystem},
  booktitle = 	 {Proc.\ NICTA Formal Methods Workshop on Operating Systems Verification},
  pages = 	 {73--97},
  year = 	 {2004},
  editor = 	 {Gerwin Klein},
  organization = {NICTA Technical Report 0401005T-1},
  publisher =    {National ICT Australia},
}