(Stellenbosch : Stellenbosch University, 2013-03) Durant, Kevin; Visser, Willem; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer Science.
ENGLISH ABSTRACT: The search for non-terminating paths within a program is a crucial part of software verification,
as the detection of anfinite path is often the only manner of falsifying program termination
- the failure of a termination prover to verify termination does not necessarily imply that a
program is non-terminating. This document describes the development and implementation of
two focussed techniques for investigating the non-termination of affine loops. The developed
techniques depend on the known non-termination concepts of recurrent sets and Jordan matrix
decomposition respectively, and imply the decidability of single-variable and cyclic affine loops.
Furthermore, the techniques prove to be practically capable methods for both the location of
non-terminating paths, as well as the generation of preconditions for non-termination.