大模型驱动的泛形式化软件工程实践

报告摘要: 形式化证明与其相关的程序分析，测试用例生成等各种软件工程技术在实践中被广泛用以提升软件质量。然而这些技术带来的使用代价也常常被开发者所诟病。而大模型的出现为我们带来了一种新的可能性，即低代价（由AI代劳）高可靠的形式化与软件工程手段。本次报告会介绍我们在操作系统领域的实践与思考，如何将大模型与静态分析，自动化测试，形式化证明等相结合，通过更低的成本寻找代码中的缺陷，提升软件质量。

报告人简介: 李屹，现为华为操作系统部OS内核实验室技术专家，负责鸿蒙内核形式化和程序分析工作。主要研究兴趣包括，软件的形式化证明、程序分析与安全漏洞挖掘等泛形式化领域工作，大模型与软件工程的结合以及操作系统的智能化探索。