LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions

TL;DR

This paper introduces a novel method combining Large Language Models and fuzz testing, guided by Fuzzing Guidance, to automatically generate weakest preconditions for programs, improving verification and error checking.

Contribution

It presents a new approach that integrates LLMs with fuzz testing and feedback guidance to enhance weakest precondition generation for programs.

Findings

LLMs can generate viable weakest preconditions.

Fuzzing Guidance improves the quality of generated WPs.

Effective on Java array programs benchmark.

Abstract

The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas ranging from verification to run-time error checking. This paper proposes the combination of Large Language Models (LLMs) and fuzz testing for generating WPs. In pursuit of this goal, we introduce \emph{Fuzzing Guidance} (FG); FG acts as a means of directing LLMs towards correct WPs using program execution feedback. FG utilises fuzz testing for approximately checking the validity and weakness of candidate WPs, this information is then fed back to the LLM as a means of context refinement. We demonstrate the effectiveness of our approach on a comprehensive benchmark set of deterministic array programs in Java. Our experiments indicate that LLMs are capable of producing viable candidate WPs, and that this ability can be practically enhanced through FG.