Authors:

Minh Binh Tran

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Static verification is highly beneficial for ensuring software quality but demands significant human effort in manual specification writing. This is particularly true for the static verification of heap-manipulating programs with separation logic. While advancements in large language models demonstrate promise in various software engineering tasks, including invariant generation, a comprehensive assessment of such models' capabilities to produce separation logic-based specifications remains unexplored. This project bridges this gap by demonstrating the effectiveness of 3 popular LLMs in generating verifiable specifications for C programs in VeriFast. Our methodology involves performing rigorous data collection by prompting 3 such models in a sparse-split approach and conducting detailed qualitative analysis of their generated outputs. The study will compare these outputs against publicly available VeriFast benchmarks to thoroughly assess their accuracy, completeness, and adherence to conventional VeriFast specification patterns. The results are expected to provide critical insights into the specific strengths and limitations of current large language models regarding these qualitative aspects. Ultimately, this research aims to contribute actionable recommendations that will guide the development of more reliable and efficient AI-driven approaches to automate formal software verification. Keywords: Static Verification; VeriFast; Large Language Models; Qualitative Analysis; Separation Logic

Source:

Purdue University / 2025

Topics:

No topics listed

Co-authors:

Minh Binh Tran