A Compositional Method for Deciding Program Termination

One of the major challenges in computer science is to put programming on a firmer mathematical basis, in order to improve the correctness of programs. This paper describes a concrete implementation of a semantic-based approach for verifying termination of open nondeterministic programs with finite data types. The presentation is focused on Erratic Idealized Algol, which represents a nondeterministic programming language that embodies many of the core ingredients of imperative and higher-order functional languages. The fully abstract game semantics of the language is used to obtain a compositional, incremental way of generating accurate models of programs. The CSP process algebra is used as a concrete formalism for representation of game models and their efficient verification. Termination of programs is decided by checking divergence-freedom of CSP processes using the FDR tool. The effectiveness of this method is presented by several examples.