Using Dependent Types to Certify the Safety of Assembly Code.

Matthew Harren, George C. Necula

Browse the full SAS paper archive.