Investigating the non-termination of affine loops

Simple item page
dc.contributor.advisorVisser, Willemen_ZA
dc.contributor.authorDurant, Kevinen_ZA
dc.contributor.otherStellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer Science.en_ZA
dc.date.accessioned2013-02-20T09:26:29Zen_ZA
dc.date.accessioned2013-03-15T07:33:03Z
dc.date.available2013-02-20T09:26:29Zen_ZA
dc.date.available2013-03-15T07:33:03Z
dc.date.issued2013-03en_ZA
dc.descriptionThesis (MSc)--Stellenbosch University, 2013.en_ZA
dc.description.abstractENGLISH 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.en_ZA
dc.description.abstractAFRIKAANSE 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.af_ZA
dc.format.extent114 p. : ill.
dc.identifier.urihttp://hdl.handle.net/10019.1/80052
dc.language.isoen_ZAen_ZA
dc.publisherStellenbosch : Stellenbosch Universityen_ZA
dc.rights.holderStellenbosch Universityen_ZA
dc.subjectTerminationen_ZA
dc.subjectAffine loopsen_ZA
dc.subjectJavaen_ZA
dc.subjectComputer software -- Verificationen_ZA
dc.subjectDissertations -- Mathematical sciencesen_ZA
dc.subjectTheses -- Mathematical sciencesen_ZA
dc.subjectDissertations -- Computer scienceen_ZA
dc.subjectTheses -- Computer scienceen_ZA
dc.titleInvestigating the non-termination of affine loopsen_ZA
dc.typeThesisen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
durant_investigating_2013.pdf
Size:
1.81 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
1.98 KB
Format:
Plain Text
Description:
Download
Collections
Masters Degrees (Mathematical Sciences)