Investigating the non-termination of affine loops

[摘要] 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 aprogram is non-terminating. This document describes the development and implementation oftwo focussed techniques for investigating the non-termination of affine loops. The developedtechniques depend on the known non-termination concepts of recurrent sets and Jordan matrixdecomposition 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 ofnon-terminating paths, as well as the generation of preconditions for non-termination.

[发布机构] Stellenbosch University