Integrating Formal Schedulability Analysis into a Verified OS Kernel. - Xiaojie Guo 003; Maxime Lesourd; Mengqi Liu 001; Lionel Rieg; Zhong Shao 001 (CAV (2), 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)

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. - Mengqi Liu 001; Lionel Rieg; Zhong Shao 001; Ronghui Gu; David Costanzo; Jung-Eun Kim; Man-Ki Yoon (Proc. ACM Program. Lang., 2020)

Aquila: a practically usable verification system for production-scale programmable data planes. - Bingchuan Tian; Jiaqi Gao; Mengqi Liu 001; Ennan Zhai; Yanqing Chen; Yu Zhou 008; Li Dai; Feng Yan; Mengjing Ma; Ming Tang; Jie Lu; Xionglie Wei; et al. (SIGCOMM, 2021)

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

Cetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling. - Yifan Li; Jiaqi Gao; Ennan Zhai; Mengqi Liu 001; Kun Liu; Hongqiang Harry Liu (NSDI, 2022)

Meissa: scalable network testing for programmable data planes. - Naiqian Zheng; Mengqi Liu 001; Ennan Zhai; Hongqiang Harry Liu; Yifan Li; Kaicheng Yang 001; Xuanzhe Liu; Xin Jin 008 (SIGCOMM, 2022)

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)

Automated Verification of an In-Production DNS Authoritative Engine. - Naiqian Zheng; Mengqi Liu 001; Yuxing Xiang; Linjian Song; Dong Li; Feng Han; Nan Wang; Yong Ma; Zhuo Liang; Dennis Cai; Ennan Zhai; Xuanzhe Liu; et al. (SOSP, 2023)

Sirius: Composing Network Function Chains into P4-Capable Edge Gateways. - Jiaqi Gao; Jiamin Cao; Yifan Li; Mengqi Liu 001; Ming Tang; Dennis Cai; Ennan Zhai (NSDI, 2024)

A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k Failures. - Ruihan Li; Yifei Yuan 001; Fangdan Ye; Mengqi Liu 001; Ruizhen Yang; Yang Yu; Tianchen Guo; Qing Ma; Xianlong Zeng; Chenren Xu; Dennis Cai; Ennan Zhai (SIGCOMM, 2024)