Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers

Varun Bharti, Shashwat Jha, Dhruv Kumar +1

Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for…