Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Investigating the non-termination of affine loops
Thesis (MSc)--Stellenbosch University, 2013.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2013
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613990135267328 |
|---|---|
| access_status_str | Open Access |
| author | Durant, Kevin |
| author2 | Visser, Willem |
| author_browse | Durant, Kevin Visser, Willem |
| author_facet | Visser, Willem Durant, Kevin |
| author_sort | Durant, Kevin |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--Stellenbosch University, 2013. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/80052 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:44:55.028Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2013 |
| publishDateRange | 2013 |
| publishDateSort | 2013 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/80052 Investigating the non-termination of affine loops Durant, Kevin Visser, Willem Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer Science. Termination Affine loops Java Computer software -- Verification Dissertations -- Mathematical sciences Theses -- Mathematical sciences Dissertations -- Computer science Theses -- Computer science 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. 2013-02-20T09:26:29Z 2013-03-15T07:33:03Z 2013-02-20T09:26:29Z 2013-03-15T07:33:03Z 2013-03 Thesis http://hdl.handle.net/10019.1/80052 en_ZA Stellenbosch University 114 p. : ill. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Termination Affine loops Java Computer software -- Verification Dissertations -- Mathematical sciences Theses -- Mathematical sciences Dissertations -- Computer science Theses -- Computer science Durant, Kevin Investigating the non-termination of affine loops |
| title | Investigating the non-termination of affine loops |
| title_full | Investigating the non-termination of affine loops |
| title_fullStr | Investigating the non-termination of affine loops |
| title_full_unstemmed | Investigating the non-termination of affine loops |
| title_short | Investigating the non-termination of affine loops |
| title_sort | investigating the non termination of affine loops |
| topic | Termination Affine loops Java Computer software -- Verification Dissertations -- Mathematical sciences Theses -- Mathematical sciences Dissertations -- Computer science Theses -- Computer science |
| url | http://hdl.handle.net/10019.1/80052 |
| work_keys_str_mv | AT durantkevin investigatingthenonterminationofaffineloops |