This dissertation is about verifying the correctness of low-level computer programs.This is challenging because low-level programs by definition cannot use many useful abstractions of computer science. Features of high-level ...