团队研究方向介绍：

软件已成为国民经济、国防建设和人民生活基础设施的核心，“软件定义一切”、“软件使能一切”已然成为一种客观需求，并呈现快速发展态势。然而，软件的可信性令人担忧。特别是在芯片设计、航空航天、无人驾驶等安全攸关基础软件领域，微小的程序缺陷都可能导致机毁人亡的严重后果。

我们的研究团队依托于西安电子科技大学计算机科学与技术学院，计算理论与技术研究所，西安市软件可信认证关键技术重点实验室（田聪教授团队），并于2022年12月入驻广州研究院。由于计算机软件的蓬勃发展离不开其坚实的理论基础和不断拓展的前沿技术应用，我们团队一方面长期坚持软件的基础理论研究，包括形式化方法、程序设计语言、可信软件工程技术等，另一方面在理论研究的基础上，不断拓展前沿技术应用，兼顾创新引领与落地应用，研究方向包括工业技术软件化和智能化软件工程等。

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

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

B. 可信软件工程

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

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

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

D. 工业技术软件化

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

兄弟科研团队：

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

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

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

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

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

我们提供以下机会：

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

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

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

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

我们注重以下能力：

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

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

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

4. 如果善于使用类ChatGPT等大语言模型提高科研和工作效率，并且英语写作能力好一些，是个加分项：）

团队研究氛围：

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

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

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