Show simple item record  

dc.contributor.advisorMalik, Robi
dc.contributor.advisorUtting, Mark
dc.contributor.advisorPfahringer, Bernhard
dc.contributor.authorWeng, Min-Hsien
dc.date.accessioned2019-03-28T19:27:52Z
dc.date.available2019-03-28T19:27:52Z
dc.date.issued2019
dc.identifier.citationWeng, M.-H. (2019). Efficient compilation of a verification-friendly programming language (Thesis, Doctor of Philosophy (PhD)). The University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/12432en
dc.identifier.urihttps://hdl.handle.net/10289/12432
dc.description.abstractThis thesis develops a compiler to convert a program written in the verification friendly programming language Whiley into an efficient implementation in C. Our compiler uses a mixture of static analysis, run-time monitoring and a code generator to and faster integer types, eliminate unnecessary array copies and de-allocate unused memory without garbage collection, so that Whiley programs can be translated into C code to run fast and for long periods on general operating systems as well as limited-resource embedded devices. We also present manual and automatic proofs to verify memory safety of our implementations, and benchmark on a variety of test cases for practical use. Our benchmark results show that, in our test suite, our compiler effectively reduces the time complexity to the lowest possible level and stops all memory leaks without causing double-freeing problems. The performance of implementations can be further improved by choosing proper integer types within the ranges and exploiting parallelism in the programs.
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/zip
dc.language.isoen
dc.publisherThe University of Waikato
dc.rightsAll items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
dc.subjectOptimizing Compiler, Program Efficiency, Static Analysis, Formal Verification, Parallel Programming
dc.subjectProgram Efficiency
dc.subjectStatic Analysis
dc.subjectFormal Verification
dc.subjectParallel Programming
dc.subjectthesis by publication
dc.titleEfficient compilation of a verification-friendly programming language
dc.typeThesis
thesis.degree.grantorThe University of Waikato
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy (PhD)
dc.date.updated2019-03-25T22:45:35Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record