文成，西安电子科技大学广州研究院华山准聘副教授（讲师），硕士生导师，CCF形式化方法专委会通讯委员。2022年12月于深圳大学计算机科学与技术专业获得工学博士学位（导师：秦胜潮教授）；在此之前曾在新加坡南洋理工大学访学一年，在华为技术有限公司可信理论、技术与工程实验室进行产业实践两年。目前主要从事高可信软件工程技术、人工智能使能软件开发与验证、可信软件的基础理论与方法等方面的研究，坚持理论研究与产业应用并重，目前已经在包括ICSE 2024，ICSE 2022，ICSE 2020，IEEE Transactions on Reliability等顶级国际会议和期刊上发表十余篇论文；作为项目负责人承担国家自然科学基金青年基金项目1项、中国博士后科学基金面上项目1项，以及华为公司企业产学研合作课题1项。个人独立研发的自动化测试工具集已在Linux系统主流的开源应用程序中发现上百个真实缺陷（包括73 CVEs），主导研发的并发程序分析平台已在华为公司多个产品线得到实际部署和使用。

本人成果寥寥。但努力科研，享受电竞，热爱生活。

个人标签

业余电竞选手；云玩家；科研爱好者；电影爱好者；知乎键盘侠

研究方向

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

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

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

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

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

科研感悟

借用一位年轻的教授说的话，科研就像一场Dota比赛，搞短平快的研究（类似于dota使用一些前期厉害的英雄）虽然能使你在比赛开始大杀四方，但是由于科研后劲不足（不能深钻），后期还是会输掉比赛（被一波带走）。而研究SEC，PL和SE就类似于在Dota比赛中选择幽鬼，虽然开局会比较难混，但是基础扎实了之后（辉耀到手），你会发现可以做的东西有很多，未来的高质量论文会源源不断。所以每一个搞科研的人都必须问问自己，你是愿意选个天怒法师前期各种超神，还是愿意选个后期最后赢得胜利。选择不同，你做的科研也自然不同。

不错，科研就像一场Dota比赛！而我不仅喜欢玩幽鬼，还喜欢玩天怒法师。我喜欢拿幽鬼前期打架，也喜欢拿天怒法师打后期。科研如电竞，输赢看淡，不服就干。发不出论文也好，不能毕业也罢，不过是过眼云烟。人生苦短，路上有科研相伴，有游戏相伴。心态不同，你做的科研也不同。