A Representation of Fomega in LF. - Carsten Schürmann; Dachuan Yu; Zhaozhong Ni (MERLIN, 2001)

A Syntactic Approach to Foundational Proof-Carrying Code. - Nadeem Abdul Hamid; Zhong Shao 001; Valery Trifonov; Stefan Monnier; Zhaozhong Ni (J. Autom. Reason., 2003)

Modular verification of assembly code with stack-based control abstractions. - Xinyu Feng 001; Zhong Shao 001; Alexander Vaynberg; Sen Xiang; Zhaozhong Ni (PLDI, 2006)

Certified assembly programming with embedded code pointers. - Zhaozhong Ni; Zhong Shao 001 (POPL, 2006)

An open framework for foundational proof-carrying code. - Xinyu Feng 001; Zhaozhong Ni; Zhong Shao 001; Yu Guo (TLDI, 2007)

Using XCAP to Certify Realistic Systems Code: Machine Context Management. - Zhaozhong Ni; Dachuan Yu; Zhong Shao 001 (TPHOLs, 2007)

Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor. - Zhenyang Dai; Shuang Liu; Vilhelm Sjöberg; Xupeng Li; Yu Chen 004; Wenhao Wang 001; Yuekai Jia; Sean Noble Anderson; Laila Elbeheiry; Shubham Sondhi; Yu Zhang; Zhaozhong Ni; et al. (ASPLOS (2), 2024)