Investigating the non-termination of affine loops

Description

Thesis (MSc)--Stellenbosch University, 2013. / 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. / AFRIKAANSE OPSOMMING: Sagtewareveri kasie vereis of die bewys van die beeindiging van 'n program, of die deteksie
van oneindige uitvoerings. In hierdie tesis ontwikkel en implementeer ons twee tegnieke om
oor die oneindige eienskap van a ene lusse te beslis. Die tegnieke wat ontwikkel word is
gebaseer op konsepte soos Jordan matriksdekomposisie en herhaalde groepe wat al in die verlede
gebruik is om die beeindiging van lusse te ondersoek. Die tegnieke kan gebruik word om
die uitvoerbaarheid van beide een-veranderlike en sikliese a ene lusse te bepaal. Feitlik alle
nie-eindige a ene lusse kan ge denti seer word en die toestande waaronder hierdie oneindige
eienskap verskyn kan beskryf word.

Links & Downloads

1. http://hdl.handle.net/10019.1/80052

Tags

Termination

Affine loops

Java

Computer software -- Verification

Dissertations -- Mathematical sciences

Theses -- Mathematical sciences

Dissertations -- Computer science

Theses -- Computer science

Additional Fields

Identifer	oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/80052
Date	03 1900
Creators	Durant, Kevin
Contributors	Visser, W., Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer Science.
Publisher	Stellenbosch : Stellenbosch University
Source Sets	South African National ETD Portal
Language	en_ZA
Detected Language	English
Type	Thesis
Format	114 p. : ill.
Rights	Stellenbosch University