Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).

Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen

Browse the full ITP paper archive.