CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Xiongnan (Newman) Wu; Jieung Kim; Vilhelm Sjöberg; David Costanzo (OSDI, 2016)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. - Hao Chen 023; Xiongnan (Newman) Wu; Zhong Shao 001; Joshua Lockerman; Ronghui Gu (J. Autom. Reason., 2018)

Building certified concurrent OS kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Jieung Kim; Jérémie Koenig; Xiongnan (Newman) Wu; Vilhelm Sjöberg; David Costanzo (Commun. ACM, 2019)

A new hierarchical software architecture towards safety-critical aspects of a drone system. - Xiaorui Zhu; Chen Liang; Zhen-guo Yin; Zhong Shao 001; Meng-qi Liu 001; Hao Chen 023 (Frontiers Inf. Technol. Electron. Eng., 2019)

Blinder: Partition-Oblivious Hierarchical Scheduling. - Man-Ki Yoon; Mengqi Liu 001; Hao Chen 023; Jung-Eun Kim; Zhong Shao 001 (USENIX Security Symposium, 2021)

Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation. - Mengqi Liu 001; Zhong Shao 001; Hao Chen 023; Man-Ki Yoon; Jung-Eun Kim (Proc. ACM Program. Lang., 2022)

A NAND Use Case for Cybersecurity Experiments. - Timothy Fraser; Xuwei Liu; Qingkai Shi; Xiangyu Zhang 001; Mark Wutka; Daniel Balasubramanian; Hao Chen 023; Zhong Shao 001 (SecDev, 2024)

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. - Jieung Kim; Jérémie Koenig; Hao Chen 023; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)