Verifying Preemptive Kernel Code with Preemption Control Support. - Yu Guo; Haozhong Zhang (TASE, 2014)

Formal Verification of Interrupt Injection in a Hypervisor. - Haozhong Zhang; Yu Guo (TASE, 2014)

Deep Specifications and Certified Abstraction Layers. - Ronghui Gu; Jérémie Koenig; Tahina Ramananandro; Zhong Shao 001; Xiongnan (Newman) Wu; Shu-Chun Weng; Haozhong Zhang; Yu Guo (POPL, 2015)

MDev-NVMe: A NVMe Storage Virtualization Solution with Mediated Pass-Through. - Bo Peng; Haozhong Zhang; Jianguo Yao; Yaozu Dong; Yu Xu; Haibing Guan (USENIX ATC, 2018)