西电计科院华山准聘副教授、硕导，CCF形式化方法专委会通讯委员。

- 2016：电子科技大学，软件工程（本科）；

- 2018：日本早稻田大学，计算机科学与技术（分布式操作系统），导师：小柳惠一；

- 2022：航天五院502所，控制科学与工程博士（航天嵌入式系统），导师：杨孟飞。

研究方向：嵌入式操作系统、形式化验证、空间飞行器控制系统、智能测试验证。

科研经历：

- 参与我国第四代空间操作系统SpaceOS研发，负责架构设计与验证，已应用于嫦娥、天宫等重大航天工程；

- 主持1项国家级纵向课题，9项产学研横向合作课题，参与3项国家级科研项目；

- 研发工具平台已在航天型号产品中落地部署；

- 成果发表于ASE、ACM MM、Information Fusion、软件学报等会议/期刊；

- 毕业后加入田聪教授领衔的计算理论与技术研究所（ICTT），坚持“理论+工程”并重，聚焦航天软件可信保障。

常年招收喜欢嵌入式软件、硬件方向并向往星辰大海的硕士与博士研究生，以及有余力的优秀本科生（参与实践有劳务费哟）。招生渠道有两个，分别是西安电子科技大学（西安）与航天五院502所（北京），欢迎联系！

2026年保研工作已结束，所有名额已满。

Paper2026：

[1] Ma Z, Xiao Liang, Wen C, Chen R, Gu B, Qin S, Tian C, Yang M. Automated LTL Specification Generation from Industrial Aerospace Requirements. Proceedings of the 27th International Symposium on Formal Methods. 2026. (FM 2026, CCF-A).

[2] Ma Z, Wen C, Yu B, Su J. Integrating ensemble learning and Large Language Models for efficient formal verification of IP-based aerospace systems. Information Fusion. (INFFUS 2026, 中科院一区).

[3] Wen C, Ma Z, Hu J, Wang J, Su J, Xu Z, Liu D, Tian C, Yang M. A Review on Software Formal Verification Empowered by Large Language Models. Journal of Software. (in Chinese). 2026. (软件学报 2026, CCF中文T1类).

Paper2025：

[1] Ma Z, Wen C, Su Z, Liang X, Tian C, Qin S, Yang M. Bridging Natural Language and Formal Specification - Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs. The 40th IEEE/ACM International Conference on Automated Software Engineering. (ASE 2025, CCF-A，杰出论文奖).

[2] 李春奕, 马智, 武强, 王小兵, 赵亮. 基于时序逻辑的需求文本隐含语义解析与推理. (软件学报，中文CCF-A).

[3] Liang X, Hu J, Wang D, Ma Z*, Zhao L, Li R, Wan B, Wang Q. CheXPO: Preference Optimization for Chest X-ray VLMs with Counterfactual Rationale. Proceedings of the 33rd ACM International Conference on Multimedia. (ACM MM 2025, CCF-A).

[4] Liang X, Liu C, Ma Z*, Wang D, Jing B, Wang Q, Shi Y. Anatomical Region-Guided Contrastive Decoding: A Plug-and-Play Strategy for Mitigating Hallucinations in Medical VLMs. Proceedings of the AAAI Conference on Artificial Intelligence. (AAAI 2026 Oral, CCF-A).

[5] Feng D, Xu J, Li K, Ma Z*, Li W, Wang D. Fadet: A Frequency-aware Detection Framework for Infrared Small Target Detection. IEEE Journal of Selected Topics in Applied Earth Observations and Remote Sensing. (IEEE J-STARS 2025, 中科院二区期刊).

课题挑战：

A. 面向空间飞行器的嵌入式操作系统设计

随着我国星网技术的迅猛发展，空间飞行器对嵌入式操作系统的设计提出了前所未有的严峻挑战。这些挑战主要体现在：如何在极端空间辐射环境下，保证操作系统具备卓越的容错与鲁棒性；如何在高并发、海量数据传输与处理的需求下，实现严格的硬实时性能与精细的资源优化；如何应对复杂网络互联和多任务调度的复杂性；以及如何在有限资源和高风险环境下，实现操作系统在轨动态升级与维护的安全性、可靠性与可管理性，同时满足空间任务对操作系统的高可信认证要求。 为应对这些核心挑战，团队提出了 SpaceOS-Linux的研究规划，这是一个基于开源操作系统Linux的深度定制与加固版本，旨在满足空间恶劣环境下的高可靠、硬实时、低功耗及抗辐射等特殊需求，并支持在轨软件动态配置与升级，为下一代空间飞行器提供高性能、高可信的基础软件平台。欢迎对嵌入式操作系统感兴趣的同学加入！

B. 面向嵌入式软件的智能体研发

嵌入式软件需要经常和底层硬件交互，而大模型在处理这种低层级、资源受限且对实时性有严格要求的开发任务时，普遍表现较差。这给面向嵌入式软件的智能体研发带来了前所未有的严峻挑战。这些挑战主要体现在：如何在有限的计算资源和内存环境下，使智能体有效理解并生成针对特定微控制器、传感器和外设的底层驱动代码；如何确保所生成代码满足严格的实时性、高可靠性与安全性要求；如何实现对硬件抽象层、寄存器操作等细节的精确控制与代码优化；以及如何将智能体能力与嵌入式系统特有的编译、调试、烧录及在环仿真流程深度融合。 为应对这些核心挑战，团队提出了面向嵌入式软件的智能体研发规划，旨在探索如何构建能够理解硬件特性、生成高效底层代码并辅助验证的可信智能体，从而显著提升嵌入式软件的开发效率与质量。欢迎对智能代码生成、嵌入式系统和软硬协同设计感兴趣的同学加入！

C. 面向载人登月重大工程的月球车控制系统研发
载人登月任务对月球车的自主性和可靠性提出了极高的要求，其控制系统的研发面临着前所未有的严峻挑战。这些挑战主要体现在：如何在月球极端温度、高辐射和月尘环境下，确保控制系统硬件的稳定性和软件的鲁棒性；如何在缺乏全球定位系统（GPS）的月面，实现高精度、高可靠的自主导航、定位与路径规划；如何有效融合多源传感器信息，实现复杂地形的感知和智能避障；如何应对地月间通信长延时对遥操作控制稳定性和实时性的影响；以及如何设计一套高度安全、容错且支持在轨动态重构的控制架构，以保障宇航员安全和任务关键操作的顺利进行。 为应对这些核心挑战，团队提出了基于载人登月的月球车控制系统研发规划，旨在探索智能自主导航与决策、高精度感知与环境建模、鲁棒遥操作与人机协同控制，以及高可靠软硬件一体化设计等关键技术，为未来我国载人月球探测任务提供安全、高效、智能的移动平台。欢迎对机器人控制、自主导航、高可靠系统设计和人机交互感兴趣的同学加入！

合作科研单位：

1. 计算理论与技术研究所广州研究院

2. 北京控制工程研究所（502所）

3. 华为技术有限公司（2012实验室）

我们提供以下机会：

1. 参与国家重大科研项目与航天工程实践项目，提供相应高性能服务器计算资源和周边资源。

2. 支持有较强科研能力的同学发表高水平研究论文、申请国家发明专利，以及参加国内外学术会议和论坛。

3. 支持有较强动手能力的同学到兄弟科研单位等业界领先企业实习。

4. 推荐表现优秀的同学继续攻读杨孟飞老师的工学博士，或到国内外优秀大学攻读博士学位。

5. 工作推荐，优先内推工程能力极强的同学去502、504、631、771等头部军工企业工作。