2025/07/03 by Daragh King, King, Daragh, Vasileios Koutavas +3
Computer Science · #Artificial Intelligence (cs.AI) #Benchmark (surveying) #Context (archaeology) #FOS: Computer and information sciences #Formal Methods in Verification #Fuzz testing #Logic in Computer Science (cs.LO) #Parallel Computing and Optimization Techniques #Set (abstract data type) #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #Task (project management)
paper · pdf · doi:10.48550/arxiv.2507.05272
openalex publication_date 2025/07/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
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 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.