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 for verification

Hamilton, Geoff orcid logoORCID: 0000-0001-5954-6444 (2007) Distilling programs for verification. Electronic Notes in Theoretical Computer Science, 190 (4). pp. 17-32. ISSN 1571-0661

Abstract
In this paper, we show how our program transformation algorithm called distillation can not only be used for the optimisation of programs, but can also be used to facilitate program verification. Using the distillation algorithm, programs are transformed into a specialised form in which functions are tail recursive, and very few intermediate structures are created. We then show how properties of this specialised form of program can be easily verified by the application of inductive proof rules. We therefore argue that the distillation algorithm is an ideal candidate for inclusion within compilers as it facilitates the two goals of program optimization and verification.
Metadata
Item Type:Article (Published)
Refereed:Yes
Uncontrolled Keywords:transformation; optimization; proof; verification
Subjects:Computer Science > Algorithms
Computer Science > Software engineering
DCU Faculties and Centres:Research Initiatives and Centres > Lero: The Irish Software Engineering Research Centre
DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing
Publisher:Elsevier
Official URL:http://dx.doi.org/10.1016/j.entcs.2007.09.005
Copyright Information:Copyright © 2007 Elsevier B.V. All rights reserved.
Use License:This item is licensed under a Creative Commons Attribution-NonCommercial-Share Alike 3.0 License. View License
ID Code:17736
Deposited On:23 Jan 2013 11:42 by Geoffrey Hamilton . Last Modified 15 May 2020 11:04
Documents

Full text available as:

[thumbnail of hamilton.pdf]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
172kB
Downloads

Downloads

Downloads per month over past year

Archive Staff Only: edit this record