Selene：软件验证中自动化证明的开创性探索
软件工程
2024-06-06 v2
摘要
确保正确性是软件工程的一个关键方面。在众多可用策略中，软件验证提供了对正确性的最终保证。然而，编写验证证明耗费资源且人力密集，因此迫切需要自动化这一过程。本文介绍了 Selene，这是首个基于真实世界工业级操作系统微内核 seL4 构建的项目级自动化证明基准。Selene 为端到端的证明生成提供了一个全面的框架和一个轻量级的验证环境。我们使用先进的大语言模型（LLMs），如 GPT-3.5-turbo 和 GPT-4，进行的实验结果表明了大语言模型在自动化证明生成领域的能力。此外，我们进一步提出的增强方法表明，Selene 所呈现的挑战可以在未来的研究工作中得到缓解。
引用
@article{arxiv.2401.07663,
title = {Selene: Pioneering Automated Proof in Software Verification},
author = {Lichen Zhang and Shuai Lu and Nan Duan},
journal= {arXiv preprint arXiv:2401.07663},
year = {2024}
}