LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908716347949056 |
|---|---|
| author | King, Daragh Koutavas, Vasileios Kovacs, Laura |
| author_facet | King, Daragh Koutavas, Vasileios Kovacs, Laura |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_05272 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions King, Daragh Koutavas, Vasileios Kovacs, Laura Software Engineering Artificial Intelligence Logic in Computer Science 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. |
| title | LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions |
| topic | Software Engineering Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2507.05272 |