Authors:

Marilyn Rego

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Formal verification is a powerful method for enhancing software quality, but it demands significant human labor and resources. To address this challenge, this project evaluates the effectiveness of large language models (LLMs), specifically OpenAI's GPT models, in generating fully correct specifications for static verification of human-written programs. We tested this approach using the benchmark suite from VeriFast, a program verification tool for Java and C programs that efficiently handles concurrency and illegal memory accesses. The benchmarks were manually categorized to create three different types of input-output pairs to train and test the GPT models, where the input is the intended behavior specified by the user and the output is the fully specified program. Our first experiment employed prompt engineering on the GPT models. Based on the results, we created an extensive categorization of all the compilation and verification errors generated by the GPT models. In our second experiment, we used prompt chaining to address the errors. The results indicated that while prompt chaining significantly reduced compilation errors, it did not improve verification error rates compared to prompt engineering. We further explored few-shot learning to better accommodate proof repair. Through this structured approach, we aim to demonstrate the potential of LLMs in aiding the formal verification process, ultimately reducing the human effort required for verification tools like Verifast and thus improving software quality. Keywords: Formal Verification; Large Language Models; Prompt Engineering; Separation Logic

Source:

Purdue University / 2024

Topics:

No topics listed

Co-authors:

Marilyn Rego