Ph.D. Student in Computer Science and Technology
School of Informatics, Xiamen University
Published as Mingyuan Song
I am interested in advanced AI systems, AI infrastructure, and agent systems, drawing on my background in building reliable, efficient networked and distributed systems.
I am a Ph.D. student in the School of Informatics at Xiamen University, advised by Professor Qiao Xiang. I also receive research guidance from Qiang Su. I have published at top-tier conferences such as ACM SIGCOMM. My research focuses on network verification, AI infrastructure, and constraint-solving algorithms.
Internships on SuperPod communication modeling and system simulation at Huawei's 2012 Network Technology Lab and development for an A/B testing platform at Tencent shaped my interest in the interconnects, simulation tools, and runtime systems supporting modern AI workloads.
If you are interested in my research or projects, please feel free to contact me at mingyuan.song.xmu [at] gmail.com for discussion or collaboration.
Began Ph.D. studies in the School of Informatics at Xiamen University, advised by Professor Qiao Xiang.
Our paper Procurator on verifying distributed in-network computing programs was published at ACM SIGCOMM 2026.
ACM SIGCOMMCompleted the M.S. in Computer Technology at Xiamen University.
Our paper LEOPARD on cloud access-control policy verification was published at IEEE/ACM IWQoS 2025.
IEEE/ACM IWQoSMy research connects formal verification and cross-layer system simulation with open design questions in AI infrastructure and multi-agent runtimes.
How do cluster interconnects, memory hierarchies, and runtime schedulers shape distributed training and inference efficiency? Building on SuperPod communication modeling, I am interested in how transport protocols, collective primitives, and resource multiplexing behave under dynamic AI workloads.
Multi-step tool invocation, external state mutation, and asynchronous message passing make multi-agent workflows difficult to coordinate and debug. I am interested in how execution tracing, state isolation, and formal verification methods can make agent runtimes predictable and verifiable.
My published research builds verification and hardware-acceleration mechanisms for networked and cloud systems. Using reactive actor modeling, intermediate-representation pruning, logical encoding reduction, and programmable switch pipelines, these systems verify distributed P4 programs, check cloud access-control policies, and accelerate SAT search.
Building on practical experience in network and communication simulation, I am interested in developing efficient, scalable, and accurate simulation methodologies to analyze the system behavior of modern AI infrastructure.
This practice involves event-driven simulation of emerging interconnect architectures, modeling cross-layer protocol behavior and communication patterns to examine end-to-end data movement across distributed AI systems.
Open-source verifier for distributed stateful P4 systems. Compiles declarative network specifications and imported P4 programs into Boogie harnesses, then invokes Ultimate/GemCutter to check bounded safety properties and emit counterexample witnesses.
Portable multi-agent orchestration workflow for software feature delivery. Coordinates parallel work packages through explicit interface contracts, non-overlapping file ownership, single-integrator staging, consolidated feature review, and real-boundary runtime verification.
Experimental Rust library for allocation-free multiprecision multiplication, squaring, and modular slice arithmetic. Proves functional refinement in Verus across schoolbook, Karatsuba, Toom-3, and low-product kernels, alongside packed-convolution composition theorems.
Procurator verifies distributed in-network P4 programs by modeling programmable switch pipelines as reactive actors communicating via message passing, combining intermediate-representation pruning and schedule replay to reduce state-space exploration.
@inproceedings{procurator2026,
title = {Towards Efficient Verification of Distributed In-Network Computing Programs},
author = {Song, Mingyuan and Shen, Huan and Jiang, Jinghui and Su, Qiang and Zhang, Ziheng and Song, Qingyu and Zhang, Yuchao and Feng, Wanjian and Yuan, Fei and Xing, Yitao and Wei, Wenjia and Xiang, Qiao and Shu, Jiwu},
booktitle = {Proceedings of the ACM SIGCOMM 2026 Conference},
year = {2026},
pages = {74--91},
doi = {10.1145/3789240.3829122},
url = {https://doi.org/10.1145/3789240.3829122}
}LEOPARD accelerates SMT-based verification of cloud access-control policies through logical encoding optimization, applying structure-based and semantics-based pruning to remove redundant formulas unrelated to the target verification property.
@inproceedings{leopard2025,
title = {{LEOPARD}: Accelerating Cloud-based Access Control Policy Verification Using Logical Encoding Optimization},
author = {Fang, Xing and Ding, Feiyan and Song, Mingyuan and Zhao, Yuntao and You, Lizhao and Xiang, Qiao and Kong, Linghe and Shu, Jiwu and Liu, Xue},
booktitle = {2025 IEEE/ACM 33rd International Symposium on Quality of Service (IWQoS)},
year = {2025},
pages = {1--10},
doi = {10.1109/iwqos65803.2025.11215174},
url = {https://doi.org/10.1109/iwqos65803.2025.11215174}
}This work offloads Boolean satisfiability solving onto programmable switching ASICs, using match-action tables and TCAM to check variable assignments while driving search through data-plane registers and packet mirroring.
@inproceedings{sat2023,
title = {Accelerating {SAT} Solving Using Switching {ASICs}},
author = {Huang, Zhenpei and Fan, Xiwen and Jiang, Jinghui and Song, Mingyuan and Tang, Lu and Xiang, Qiao and Shu, Jiwu},
booktitle = {2023 IEEE 29th International Conference on Parallel and Distributed Systems (ICPADS)},
year = {2023},
pages = {1983--1990},
doi = {10.1109/icpads60453.2023.00271},
url = {https://doi.org/10.1109/icpads60453.2023.00271}
}