On Termination of Integer Linear Loops

TL;DR

This paper presents a decision procedure for determining the termination of simple linear integer loops with diagonalisable matrices, leveraging advanced mathematical tools, marking a significant progress on a longstanding open problem.

Contribution

It introduces the first decision procedure for loop termination under these conditions, using algebraic, number theoretic, and geometric methods.

Findings

Decidability of loop termination established for diagonalisable matrices.

Novel application of algebraic and analytic number theory in program verification.

Addresses a 10-year-old open problem in the field.

Abstract

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, u, a, and c are integer vectors, and A and B are integer matrices. Assuming the matrix A is diagonalisable, we give a decision procedure for the problem of whether, for all initial integer vectors u, such a loop terminates. The correctness of our algorithm relies on sophisticated tools from algebraic and analytic number theory, Diophantine geometry, and real algebraic geometry. To the best of our knowledge, this is the first substantial advance on a 10-year-old open problem of Tiwari (2004) and Braverman (2006).