Automated correctness proofs of machine code programs for a commercial microprocessor