Skip to main content
DORAS
DCU Online Research Access Service
Login (DCU Staff Only)
Distilling programs for verification

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

Full text available as:

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
172kB

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.

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

Downloads

Downloads per month over past year

Archive Staff Only: edit this record

Altmetric
- Altmetric
+ Altmetric
  • Student Email
  • Staff Email
  • Student Apps
  • Staff Apps
  • Loop
  • Disclaimer
  • Privacy
  • Contact Us