REVIEW 2 cited by
Selene: Pioneering Automated Proof in Software Verification
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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 operating system microkernel, seL4. Selene provides a comprehensive framework for end-to-end proof generation and a lightweight verification environment. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of 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.
Forward citations
Cited by 2 Pith papers
-
RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
Retrieval-augmented prompting improves LLM proof-completion pass rates by 27% relative on a new repository-level Verus benchmark and triples them on a function-level benchmark at low sampling budgets.
-
A Contemporary Survey of Large Language Model Assisted Program Analysis
A review that catalogs how large language models are used in static, dynamic, and hybrid program analysis, and outlines open challenges.
Discussion (0). Continue with ORCID to comment.