@article{YangH11,
  author    = {Jean Yang and
               Chris Hawblitzel},
  title     = {Safe to the last instruction: automated verification of
               a type-safe operating system},
  journal   = {Commun. ACM},
  volume    = {54},
  number    = {12},
  year      = {2011},
  pages     = {123-131},
}