On Termination of Integer Linear Loops

Joël Ouaknine, João Sousa Pinto, James Worrell

A fundamental problem in program verification concerns the termination of simple linear loops of the form x := u ; while Bx >= b do {x := Ax + a} where x is a vector of variables,…