Abstract :

Rice's theorem states that any non-trivial property of recursive sets is undecidable, and the halting problem is the generic undecidable problem. And yet, a paper in CACM 2009 observes in its sub-title, "In contrast to popular belief, proving termination is not always impossible". The new century has seen many new results proving termination for specific classes of infinite state systems. In this talk, we present one technique, namely the use of well-quasi orders for proving termination. We illustrate it with an old proof that has led many recent applications.