quadratic invariants

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. …