Linear Loop Synthesis for Quadratic Invariants

S. Hitarth, George Kenison, Laura Kovács +1

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task a…