A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning

Daragh King, Vasileios Koutavas, Laura Kovacs

Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, ye…