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, {em 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.