On Termination of Linear Programs and the Skolem Problem

James Worrell
Oxford Computing Laboratory
Friday, 28 November, 2008 (All day)

A central problem in software verification concerns the termination of linear programs, i.e. programs consisting of WHILE loops in which the guards, conditionals, and assignments are all linear (or affine). Consider the case of simple WHILE loops without conditionals, i.e., programs of the form: WHILE (Ax > c) do {x := Bx + d} where c and d are vectors, A and B are matrices, and x is a vector of variables. A longstanding open problem is whether termination for such programs is decidable, given an initial value for x. I will discuss some progress and ongoing work on this question, as well as relationships to the Skolem problem in number theory, and to the analysis of Markov chains. This is joint work with Matt Daws and Joel Ouaknine