Hamilton, Geoff ORCID: 0000-0001-5954-6444 (2020) Distilling programs to prove termination. In: 8th International Workshop on Verification and Program Transformation, 25-26 Apr 2020, Dublin, Ireland.
Abstract
The problem of determining whether or not any program terminates was shown to be undecidable by Turing, but recent advances in the area have allowed this information to be determined for a large class of programs. The classic method for deciding whether a program terminates dates back to Turing himself and involves finding a ranking function that maps a program state to a well-order, and then proving that the result of this function decreases for every possible program transition. More recent approaches to proving termination have involved moving away from the search for a single ranking function and toward a search for a set of ranking functions; this set is a choice of ranking functions and a disjunctive termination argument is used. In this paper, we describe a new technique for determining whether programs terminate. Our technique is applied to the output of the distillation program transformation that converts programs into a simplified form called distilled form. Programs in distilled form are converted into a corresponding labelled transition system and termination can be demonstrated by showing that all possible infinite traces through this labelled transition system would result in an infinite descent of well-founded data values. We demonstrate our technique on a number of examples, and compare it to previous work.
Metadata
Item Type: | Conference or Workshop Item (Paper) |
---|---|
Event Type: | Conference |
Refereed: | Yes |
Subjects: | UNSPECIFIED |
DCU Faculties and Centres: | DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing |
Published in: | Proceedings 8th International Workshop on Verification and Program Transformation (VPT'20). Electronic Proceedings in Theoretical Computer Science 320. Open Publishing Association (EPTCS). |
Publisher: | Open Publishing Association (EPTCS) |
Official URL: | http://eptcs.web.cse.unsw.edu.au/paper.cgi?VPTHCVS... |
Copyright Information: | © 2020 The Author (CC-BY 4.0) |
ID Code: | 25844 |
Deposited On: | 13 May 2021 11:11 by Geoffrey Hamilton . Last Modified 13 May 2021 11:11 |
Documents
Full text available as:
Preview |
PDF
- Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
280kB |
Downloads
Downloads
Downloads per month over past year
Archive Staff Only: edit this record