IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2008 > Proving Termination One Loop at a Time

Tuesday, April 29, 2008

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

Samir Genaim, Post-doctoral Researcher, Technical University of Madrid (UPM), Spain

Proving Termination One Loop at a Time

Abstract:

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.