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

Daragh King, Vasileios Koutavas, Laura Kovacs

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 gener…