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 self-modifying code. - Hongxu Cai; Zhong Shao 001; Alexander Vaynberg (PLDI, 2007)

CertiKOS: a certified kernel for secure cloud computing. - Liang Gu; Alexander Vaynberg; Bryan Ford; Zhong Shao 001; David Costanzo (APSys, 2011)

Compositional Verification of a Baby Virtual Memory Manager. - Alexander Vaynberg; Zhong Shao 001 (CPP, 2012)