Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.

Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen

Browse the full ITP paper archive.