From Polynomial Invariants to Linear Loops

George Kenison, Laura Kovács, Anton Varonka

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verific…