Finding Inductive Loop Invariants using Large Language Models

Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty +6

Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become u…