Safe to the last instruction: automated verification of a type-safe operating system.

Jean Yang, Chris Hawblitzel

Browse the full PLDI paper archive.