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

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

高可信软件工程

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

轻量级软件分析

工业技术软件化

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

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

  

• 高可信软件工程

  软件工程以提高软件生产率和软件质量为目标，高可信软件工程是其面向可信性性质的重要技术组成。团队致力于探索以形式化方法为基础的高可信软件工程技术，研究如何在软件的设计、开发和验证等阶段保证软件具有正确性、可靠性、安全性等高可信性质。团队的在研课题包括：（1）软件设计阶段可信技术：基于Event-B的系统级建模与分析方法研究、面向协议文本描述的自动或辅助建模技术研究、SysML/AADL行为模型到形式化模型到转换技术研究；（2）软件开发阶段可信技术：基于非正确性分离逻辑（Incorrectness Separation logic）的静态分析技术研究、基于高阶分离逻辑的Rust编译器验证技术研究；（3）软件验证阶段可信技术：基于抽象解释的C程序内存安全验证技术研究、C程序循环不变式自动生成技术研究、汇编代码验证技术研究。

  

• 人工智能使能 &
  软件开发与验证

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

  

• 轻量级软件分析

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

  

• 工业技术软件化

  工业软件是承载了工业知识和经验，面向工业领域，解决研发设计、生产制造、运维服务、经营管理等场景需求的一类软件。工业软件是工业的大脑，是辅助工业进行设计、创新、管理的载体，是支撑工业发展全过程的技术产物。然而工业软件技术壁垒高，研发周期长。我国工业软件国产化率低，核心技术受控，面临卡脖子风险。本团队致力于研究如何设计“构造即正确”的工业软件、如何开发“工业知识与计算机技术跨学科技术融合”的工业软件，以及如何验证工业软件的正确性、安全性和可靠性等关键问题，旨在以可信性新技术不断促进我国工业软件创新发展，推动工业软件国产化。团队目前已在芯片设计领域探索过领域特定的形式化建模验证流程及共性方法，积累了工业领域知识，为芯片设计EDA软件的开发和验证提供了指导方法。