Symbolic execution as a basis for termination analysis

• We present a high-level, language-independent approach to semantics-based termination analysis.
• Our formulation is useful for understanding the key ingredients and may provide useful insights for designing new tools.
• The main concepts are illustrated with an imperative and a functional language, so they are accessible to a broader audience.

Program termination is a relevant property that has been extensively studied in the context of many different formalisms and programming languages. Traditional approaches to proving termination are usually based on inspecting the source code. Recently, a new semantics-based approach has emerged, which typically follows a two-stage scheme: first, a finite data structure representing the computation space of the program is built; then, termination is analyzed by inspecting the transitions in this data structure using traditional, syntax-based techniques.Unfortunately, this approach is still specific to a programming language and semantics. In this work, we present instead a general, high-level framework that follows the semantics-based approach to proving termination. In particular, we focus on the first stage and advocate the use of symbolic execution, together with appropriate subsumption and abstraction operators, for producing a finite representation of the computations of a program. Hopefully, this higher level approach will provide useful insights for designing new semantics-based termination tools for particular programming languages.