招生信息

实验室名称：未来软件新技术实验室，又名高可信软件工程技术实验室（旧名）

实验室主页：https://xidian.work/

招生范围：博士研究生：1~2个名额，请私聊

硕士研究生：023 卓越工程师学院 --> 085404 电子信息-计算机技术 ；085412 电子信息-网络与信息安全 --> 01 粤港澳大湾区基地专项 --> 导师选：秦胜潮、文成    

导师风格：INTJ型导师，情绪稳定，多线程熬夜战神；能在组会中耐心倾听学生并给出无关痛痒的建议。希望能培养出学生独立发表顶会顶刊的能力，适合独立性强、擅长发挥主观能动性的学生。

招生信息：欢迎对软件工程、人工智能、模糊测试、形式化方法等研究方向感兴趣的同学加入我们，共同探索学术未知领域。主要招收冲顶会顶刊的学生，需要一定的代码能力，能抗住高压和push。高分通过CET-6的同学优先考虑。有意向的同学可通过邮件（wencheng [at] xidian.edu.cn）与我联系。

2022年12月入职以来，已经获批项目5项，其中国家级项目2项，厅局级项目1项，华为横向项目2项，具体信息如下：

- 深圳市基础研究专项自然科学基金，面上项目，基于程序逻辑与大语言模型的程序规约生成技术，JCYJ20250604184202003，2025年-2028年，30万元，在研，项目负责人

- 国家自然科学基金, 青年科学基金项目，面向高并发软件的可扩展建模与分析技术研究，62302375，2024年-2026年，30万元，在研，项目负责人

- 中国博士后科学基金，第73批面上资助，面向并发程序的可扩展的动态分析与测试技术研究，2023M723736，2023年-2025年，8万元，在研，项目负责人

- 华为技术有限公司，技术研究项目，面向C/C++程序的地址消毒器性能优化，TC20240717009，2024年-2025年，54.59万元，已结题，项目负责人

- 华为技术有限公司，技术研究项目，面向C/C++程序的并发测试用例辅助生成，TC20230411034，2023年-2024年，53万元，已结题，项目负责人

作为主要参与人参与的项目：

- 国家自然科学基金，面上项目，基于分离逻辑与大语言模型辅助的自动程序验证技术，62472339，2025年1月1日-2028年12月31日，在研，主要参与人

-CCF-华为胡杨林基金，形式化专项项目，基于结构化中间语言和知识图谱的需求规约自动化生成，CCF-HuaweiFM202507，2025年-2026年，在研，主要参与人

- 华为技术有限公司，技术研究项目，面向程序动静态验证的大模型训练方法和应用框架研究项目，TC20251031038，2025年-2026年，在研，主要参与人

代表性论文：

[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. 2026. (INFFUS 2026, 中科院一区，通讯作者)

[3] Wen C, Hu J, Hu Y, Su J, Yu B, Liu D, Xu Z, Sun W, Qin S, Tian C. Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations). 2026.  (ACL Demo 2026, CCF A类)

[4] Jiang C, Wang D, Liu D, Xu Z, Wen C, Ming Z, Liu Y, Wan X, Huang L. StarVerus: LLM-Powered Multi-Agent Collaboration for Industrial Rust Code Verification Automation. The 32nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining V.2. 2026. (KDD 2026, CCF A类)

[5] Jiang J, Wen C*, Fu Z, Qin S. CtxFuzz: Discovering Heap-based Memory Vulnerabilities Through Context Heap Operation Sequence Guided Fuzzing. Science of Computer Programming, Volume 249, 2026:103395 (SCP 2026, CCF B，通讯作者)

[6] Huang J, Wen C*, Su J, Xu Z, Yu B, Qin S, Tian C. Preserving Concurrency-Revealing Seeds in Fuzzing of Concurrent Programs via Tuple-Based Coverage Evaluation. Proceedings of the 33rd IEEE International Conference on Software Analysis, Evolution and Reengineering. (SANER 2026, CCF B类，通讯作者)

[7] 胡俊杰, 陈宇杰, 胡义坤, 文成*, 曹嘉伦, 马智, 苏杰, 孙纬地, 田聪, 秦胜潮. 大模型驱动的形式化定理证明：综述与展望[J].计算机科学,2026,53(04):1-23. (计算机科学, CCF中文T2类，通讯作者)

[8] 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类, ACM SIGSOFT Distinguished Paper award)

[9] Cao J，Lu Y, Li M, Ma H, Li H, He M, Wen C, Sun L, Zhang H, Qin S*, Cheung, S. C., Tian C. From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2025: 26984-27003. (ACL 2025, CCF A类)

[10] Xin G, Xu G, Zhang Y, Wen C, Zhang C, Xie X, ... & Gao P. IRHunter: Universal Detection of Instruction Reordering Vulnerabilities for Enhanced Concurrency in Distributed and Parallel Systems. IEEE Transactions on Parallel and Distributed Systems. (TPDS 2025, CCF A类, 中科院一区)

[11] Wen C, Cao J*, Su J, Xu Z, Qin S*, He M, Li H, Cheung, S. C., Tian C. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification. Proceedings of the 36th International Conference on Computer Aided Verification. 2024. (CAV 2024, CCF A类)

[12] Xu Z, Wu B, Wen C*, Zhang B, Qin S*, He M. RPG: Rust Library Fuzzing with Pool-based Fuzz Target Generation and Generic Support. Proceedings of the 46th International Conference on Software Engineering. 2024. (ICSE 2024, CCF A类，通讯作者)

[13] Wen C, Cai Y, Zhang Bin, Su J*, Xu Z, Liu D, Qin S*, Ming Z, Tian C. Automatically Inspecting Thousands of Static Bug Warnings with Large Language Model: How Far Are We? Transactions on Knowledge Discovery from Data. 2024. (TKDD , CCF B类)

[14] Wen C, He M*, Wu B, et al. Controlled concurrency testing via periodical scheduling. Proceedings of the 44th International Conference on Software Engineering. 2022: 474-486. (ICSE 2022, CCF A类)

[15] Wen C, Wang H*, Li Y, et al. Memlock: Memory usage guided fuzzing. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 2020: 765-777. (ICSE 2020, CCF A类，第一作者)

[16] Wang H, Xie X, Li Y, Wen C, et al. Typestate-guided fuzzer for discovering use-after-free vulnerabilities. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 020: 999-1010. (ICSE 2020, CCF A类)

[17] Xu Z, Wen C, Qin S*. Type learning for binaries and its applications. IEEE Transactions on Reliability, 2019, 68(3): 893-912. (SCI, 中科院二区)

[18] Xu Z, Wen C, Qin S*. State-taint analysis for detecting resource bugs. Science of Computer Programming, 2018, 162: 93-109.  (SCI, CCF B类)

[19] Xu Z, Xiong H, Wen C, Qin S*. Extracting Automata from Neural Networks Using Active Learning. National Conference on Formal Methods and Applications (FMAC). Chongqin, China. 3-4th Nov 2018.(Best Paper Award)

[20] Xu Z, Wen C, Qin S*, Ming Z. Effective malware detection based on behaviour and data features. International Conference on Smart Computing and Communication (SmartCom). Springer, Cham, Shenzhen, China. 12-14th Dec 2017. (Best Student Paper Award)

其它论文：Cheng Wen - 论文成果

Google Scholar主页：‪Cheng Wen‬ - ‪Google 学术搜索‬

ORCID主页：Cheng Wen (0000-0003-1826-6213) - ORCID

DBLP主页：Cheng Wen - DBLP‪

团队介绍：

我们的研究团队隶属于西安电子科技大学广州研究院，是由校本部计算理论与技术研究所（Institute of Computing Theory and Technology, ICTT）原班核心成员建立和发展起来的，由田聪教授担任团队负责人，秦教授担任顾问及指导，小组核心成员由3名广研院全职教师、3名西电本部兼职教师、20+名硕士研究生组成。实验室于2023年6月创建，并拟命名为高可信软件工程技术实验室，以“保障大规模软件质量和可信性”为使命，重点关注人工智能、应用软件、工控系统等领域的软件质量和可信性，致力于科研创新，利用大语言模型、形式化验证、模糊测试、静态分析与符号执行等技术，进行软件的测试与验证，以及软件缺陷的自动挖掘与理解，实现大规模软件系统的质量评估。

研究方向：

软件已成为国民经济、国防建设和人民生活基础设施的核心，“软件定义一切”、“软件使能一切”已然成为一种客观需求，并呈现快速发展态势。然而，软件的可信性令人担忧。特别是在芯片设计、航空航天、无人驾驶等安全攸关基础软件领域，微小的程序缺陷都可能导致机毁人亡的严重后果。因此，我们的研究团队一直致力于从事可信软件基础理论研究与自主可控软件测试验证平台建设。由于计算机软件的蓬勃发展离不开其坚实的理论基础和不断拓展的前沿技术应用，我们团队一方面长期坚持软件的基础理论研究，包括形式化方法、程序设计语言、可信软件工程技术等，另一方面在理论研究的基础上，不断拓展前沿技术应用，兼顾创新引领与落地应用，研究方向包括人工智能使能软件开发与验证和工业技术软件化等。

A. 形式化方法 & 程序设计语言

形式化方法是基于严格数学基础，对计算机硬件和软件系统进行描述、开发和验证的技术。团队致力于研究形式化方法的数学基础、形式系统的表达能力、形式系统的推理系统及其可靠性和完备性，以及在计算系统开发和生命周期各个阶段的理论、方法、技术、工具和应用方式等。本团队的主要研究成果体现在下面几个方面：（1）程序分析基础理论，包括基于抽象解释和不动点计算的技术；（2）程序逻辑与程序验证，包括对指针程序的验证和推理技术、基于分离逻辑的程序验证技术，以及弱内存程序的验证逻辑；（3）程序统一理论、形式语义、形式化规范述语言、形式化建模与分析。

B. 可信软件工程

软件工程以提高软件生产率和软件质量为目标，可信软件工程是其面向可信性性质的重要技术组成。本团队致力于探索以形式化方法为基础的高可信软件工程技术，研究如何在软件的设计、开发和验证等阶段保证软件具有正确性、可靠性、安全性等高可信性质。团队面向复杂软件系统（高性能、高并发、多模块、嵌入式、包含汇编代码、十万行代码以上等），基于程序静态分析、程序动态分析、自动化测试等技术相结合的技术手段，研究可扩展、高精准的软件缺陷检测和质量分析技术，解决大规模复杂软件系统的缺陷与质量分析中可扩展性低、准确率低、误报率高等问题，突破软件逻辑错误、内存安全漏洞、并发缺陷难检测、难定位的难题，从而助力测试效率与软件质量的提升。团队目前已取得突破性研究成果的课题包括智能模糊测试、并发软件分析与测试、Rust程序静态分析、Rust库自动化测试、移动软件能耗分析等方面，发现百余个真实的软件缺陷和漏洞（73 CVEs），相关软件分析工具已在华为公司中得到实际部署和使用。

C. 人工智能使能软件开发与验证

作为人工智能与软件工程交叉融合的研究方向，智能化“软件工程”侧重于在为解决各种软件工程任务而研发的方法中灌输智能，而“智能软件”工程专注于解决智能软件应用领域的各种软件工程任务。近期，以ChatGPT为代表的大语言模型技术对于包括软件工程在内的很多领域都带来了巨大的冲击，它对于软件开发的颠覆性影响应该是可以预见的。本团队未来将重点关注如何结合大语言模型来生成、优化、测试和验证软件，以提高软件开发的效率和质量。本团队目前已取得的研究成果包括基于机器学习的缺陷诊断与定位方法，基于ChatGPT的程序缺陷检测及修复实证研究，团队在研的课题包括基于大语言模型的软件规约生成技术研究。

D. 工业技术软件化

工业技术软件化是工业技术、工艺经验、制造知识和方法的显性化、数字化和系统化的过程。工业技术软件化的重点在于将工业知识/技术等要素从非软件形态转化为软件形态的同时，还要用软件去定义、改变它们的形态或性质。工业与软件是相辅相成、相互促进的。该研究方向为本团队拟探索的新方向，其中，工业知识技能至关重要，形式化方法、软件工程思想应用也必不可少。本团队致力于研究如何设计“构造即正确”的工业软件、如何开发“工业知识与计算机技术跨学科技术融合”的工业软件，以及如何验证工业软件的正确性、安全性和可靠性等关键问题，旨在以可信性新技术不断促进我国工业软件创新发展，推动工业软件国产化。团队目前已在芯片设计领域探索过领域特定的形式化建模验证流程及共性方法，积累了工业领域知识，为芯片设计EDA软件的开发和验证提供了指导方法。

兄弟科研团队：

1. 计算理论与技术研究所（西电校本部），简称ICTT

2. 深圳大学软件工程研究中心-软工组

3. 华为可信测试工程实验室-费马实验室

4. 北京轩宇信息技术有限公司

5. 航天五院502所(北京控制工程研究所)

6. 光明实验室，人工智能与数字经济广东省实验室（深圳）

我们提供以下机会：

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

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

3. 支持有较强动手能力的同学到华为技术有限公司（深圳龙岗区、东莞松山湖）、北京轩宇信息技术有限公司（北京中关村）、光明实验室（深圳光明区）等业界领先的企业实习。

4. 推荐表现优秀的同学继续在广研院攻读工程博士，或到国内外优秀大学攻读博士学位。

我们注重以下能力：

1. 善于沟通，易于交流，遇到问题及时与导师和团队沟通。

2. 独立思考能力强，面对科研目标，先有自己的思路再去讨论和阅读论文。

3. 主动性强，能主动发起讨论、主动推动工作进度（与独立思考和主动性相比，学习成绩没那么重要）。

4. 对自己自信，心理素质强，在压力面前保持头脑清醒，能从容淡定地输出自己的观点。

5. 如果善于使用类Claude Code、Codex等AI工具提高科研和工作效率，并且英语写作能力好一些，是个加分项：）

团队研究氛围（受个人师门的影响，优良的作风咱们得传承）：

1. 弹性上班制。容忍睡懒觉、熬夜加班、在实验室打游戏等不良习惯和行为。当然，因人而异，因工作而异，要保质保量地完成研究任务，投入多我们也希望能产出多。我们希望同学们更加自由、灵活和专注于研究本身(^_^)。

2. 每周举办一次组会（如遇时间冲突，可以灵活调整），同学们想介绍对自己研究的新想法、问题、计划、成果都可以，或者轮流分享对论文的阅读心得和体会，自由讨论。当然，组会的目的不是为了安排工作和汇报进度，而是大家及时拉通对齐，促进分享和交流，同时推进研究进展。

3. 定期组织聚餐、聚会、出游等团建活动，增进成员们的交流、合作和友谊。以第一作者身份发表CCF A类论文，实验室额外提供激励政策。