A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processorby Zhe Hou, David Sanan, Alwen Tiu and Yang Liu19 Oct