| Aquila: a practically usable verification system for production-scale programmable data planes B Tian, J Gao, M Liu, E Zhai, Y Chen, Y Zhou, L Dai, F Yan, M Ma, M Tang, ... Proceedings of the 2021 ACM SIGCOMM 2021 Conference, 17-32, 2021 | 43 | 2021 |
| Cetus: Releasing p4 programmers from the chore of trial and error compiling Y Li, J Gao, E Zhai, M Liu, K Liu, HH Liu 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI …, 2022 | 36 | 2022 |
| Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation M Liu, L Rieg, Z Shao, R Gu, D Costanzo, JE Kim, MK Yoon Proceedings of the ACM on Programming Languages 4 (POPL), 1-31, 2019 | 27 | 2019 |
| Integrating formal schedulability analysis into a verified OS kernel X Guo, M Lesourd, M Liu, L Rieg, Z Shao Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019 | 21 | 2019 |
| Meissa: Scalable network testing for programmable data planes N Zheng, M Liu, E Zhai, HH Liu, Y Li, K Yang, X Liu, X Jin Proceedings of the ACM SIGCOMM 2022 Conference, 350-364, 2022 | 17 | 2022 |
| A new hierarchical software architecture towards safety-critical aspects of a drone system X Zhu, C Liang, Z Yin, Z Shao, M Liu, H Chen Frontiers of Information Technology & Electronic Engineering 20 (3), 353-362, 2019 | 10 | 2019 |
| Blinder:{Partition-Oblivious} hierarchical scheduling MK Yoon, M Liu, H Chen, JE Kim, Z Shao 30th USENIX Security Symposium (USENIX Security 21), 2417-2434, 2021 | 6 | 2021 |
| Sirius: Composing Network Function Chains into {P4-Capable} Edge Gateways J Gao, J Cao, Y Li, M Liu, M Tang, D Cai, E Zhai 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI …, 2024 | 4 | 2024 |
| Automated Verification of an In-Production DNS Authoritative Engine N Zheng, M Liu, Y Xiang, L Song, D Li, F Han, N Wang, Y Ma, Z Liang, ... Proceedings of the 29th Symposium on Operating Systems Principles, 80-95, 2023 | 4 | 2023 |
| A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k Failures R Li, Y Yuan, F Ye, M Liu, R Yang, Y Yu, T Guo, Q Ma, X Zeng, C Xu, ... Proceedings of the ACM SIGCOMM 2024 Conference, 228-243, 2024 | 1 | 2024 |
| Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation M Liu, Z Shao, H Chen, MK Yoon, JE Kim Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 60-88, 2022 | 1 | 2022 |
| Real-Time CertiKos: Compositional Verification of OS Kernels with Preemptive Scheduling and Temporal Isolation M Liu Yale University, 2020 | 1 | 2020 |
| Cora: Accelerating Stateful Network Applications with SmartNICs S Xi, J Gao, M Liu, J Cao, F Li, K Bu, K Ren, M Yu, D Cai, E Zhai arXiv preprint arXiv:2410.22229, 2024 | | 2024 |
| A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary 𝑘 Failures R Li, Y Yuan, F Ye, M Liu, R Yang, Y Yu, T Guo, Q Ma, X Zeng, C Xu, ... | | 2024 |
