Login (DCU Staff Only)
Login (DCU Staff Only)

DORAS | DCU Research Repository

Explore open access research and scholarly works from DCU

Advanced Search

Distilling programs to prove termination

Hamilton, Geoff orcid logoORCID: 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:

[thumbnail of 2008.02936.pdf]
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