On the Undecidability of Loop Analysis

Abstract

Our work addresses two central questions of program analysis, termination and invariant generation of loops. Already simple infinite-state systems, such as loops with assignments only, have intrinsically complex reachable sets and render variants of these problems undecidable.

In the talk, we give an account of the existing body of work on the boundary of (un-)decidability. We contribute to the line of work related to the question raised by Braverman in 2006: ``How much non-determinism can be introduced in a linear loop before termination becomes undecidable?'' We show that termination of loops with a purely non-deterministic choice between linear updates cannot be answered by an algorithm. To our knowledge, this is the most restricted setting in which undecidability has been shown. Moreover, it contrasts the case of a single linear update where termination (i.e., reachability) is known decidable.

We also turn to the problem of computing the strongest algebraic invariant of a program, that is, all polynomial relations among program variables. Despite a complete algorithm for multi-path affine programs, allowing arbitrary polynomial assignments is known to result in the unsolvability of invariant generation. We point out that negative results do not actually exploit general polynomial updates. There exists no algorithm computing strongest algebraic invariants already for programs with quadratic updates or updates guarded by affine equalities.