Termination can be thought of as the property of programs ensuring that every input is given an output in finite time. There are many programming languages, with different features and expressive resources and programs of different shapes. The notion of operational termination provides a general definition of termination which relies on the logic-based description of the operational semantics of a programming language. The key point is capturing termination as the absence of infinite inference: all proof attempts must either successfully terminate, or else fail in finite time.

The tutorial develops a generic and unifying approach to prove termination of programs in a wide range of programming languages. The starting point is a description of the operational semantics of the programming language given by means of a computational logic. The notion of (localized) operational termination provides an appropriate semantics-based definition of termination of programs as the absence of infinite proof trees in the logic. By using a number of generic methods and procedures we obtain a unified description of the termination problem as what we call an OT problem. Then, we apply an incremental proof methodology which is able to simplify the original OT problem in a divide-and-conquer style to eventually prove (or disprove) termination of the program. We also discuss some low-level aspects of the methodology as the use of fine-grain models of the termination behavior in some languages, and the use of abstractions, search, and automated reasoning techniques in the implementation of the aforementioned proof methodology.