Proving Termination One Loop at a Time

April 29, 2008

Samir Genaim


Proving Termination One Loop at a Time

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Classic techniques for proving termination of a given loop require the identification of a measure (ranking function) that maps program states to the elements of a well-founded domain. Termination is guaranteed if this measure is shown to decrease with each iteration of the loop. This is a global termination condition as it requires to decrease for every two consecutive states. For multi-path loops (e.g. loops with if statements) such ranking functions might be complex and difficult to synthesize (lexicographic order, multi-set order, etc). In recent years, systems based on local termination conditions are emerging. Here, termination is guaranteed (under some conditions) if we find a set of (simple) ranking functions, one for each path. In this talk I will present the local approach to proving termination, illustrate its formal justification, and discuss its complexity.