Selene: Pioneering Automated Proof in Software Verification
CoRR(2024)
摘要
Ensuring correctness is a pivotal aspect of software engineering. Among the
various strategies available, software verification offers a definitive
assurance of correctness. Nevertheless, writing verification proofs is
resource-intensive and manpower-consuming, and there is a great need to
automate this process. We introduce Selene in this paper, which is the first
project-level automated proof benchmark constructed based on the real-world
industrial-level project of the seL4 operating system microkernel. Selene
provides a comprehensive framework for end-to-end evaluation and a lightweight
verification environment. Our experimental results with advanced LLMs, such as
GPT-3.5-turbo and GPT-4, highlight the capabilities of large language models
(LLMs) in the domain of automated proof generation. Additionally, our further
proposed augmentations indicate that the challenges presented by Selene can be
mitigated in future research endeavors.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要