In the quest for program analysis and verification, program termination -- determining whether a given program will always halt or could execute forever -- has emerged as a pivotal component. Unfortunately, this task was proven to be undecidable by Alan Turing eight decades ago, before the advent of the first working computers! In recent years, however, great strides have been made in the automated analysis of termination of programs, from simple counter machines to Windows device drivers.
In this talk, I will focus, from a theoretical (i.e. decidability and complexity) point of view, on the special case of simple linear loops, i.e., un-nested WHILE programs with linear assignments and linear exit conditions (and no conditionals, side effects, nothing). Somewhat surprisingly, the study of termination of simple linear loops involves advanced techniques from a variety of mathematical fields, including analytic and algebraic number theory, Diophantine geometry, and real algebraic geometry. I will present an overview of known results, and discuss existing algorithmic challenges and open problems.
This is joint work with James Worrell.