Write-Once, Prove-Once: A Reusable Framework for Secure Boot Verification in Rocq.

Minjie Fan, Qiyu Wu, Kuai Yu, Gaosong Xu, Xiaoyang Wang, Jiwu Shu

Browse the full ICPADS paper archive.