White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Property-based Testing and Properties as Types: A hybrid approach to supercompiler verification

Reich, Jason S. (2013) Property-based Testing and Properties as Types: A hybrid approach to supercompiler verification. PhD thesis, University of York.

[img]
Preview
Text
Jason S Reich - Thesis.pdf
Available under License Creative Commons Attribution-Noncommercial-Share Alike 2.0 UK: England & Wales.

Download (821Kb) | Preview

Abstract

This thesis describes a hybrid approach to compiler verification. Property-based testing and mechanised proof are combined to support the verification of a supercompiler — a particular source-to-source program optimisation. A careful developer may use formal methods to ensure that their program code is correct to specifications. Poorly constructed compilers (and their associated machinery) can produce object code that does not have the same meaning as the source program. Therefore, to ensure the correctness of the executable program, each component of the compilation pipeline needs to be verified. Lazy SmallCheck — a property-based testing library — is extended with support for existential qualification, functional values and a technique for displaying partial counterexamples. Lazy SmallCheck is then applied to the efficient generation of test programs for a small first-order functional language, specified using declarative statements of program validity. We extend the technique with several definitions of canonical programs to reduce the test-data space. A supercompiler is implemented for a core higher-order language, contrasting implementations found in other publications. We also survey the techniques and themes seen in the literature on compiler proof. These surveys inform the development of an abstract verified supercompiler in a dependently-typed language. In this work, we represent correctness properties as types. This abstract model is then adapted to integrate mechanical proof and results of property-based testing to verify a working supercompiler implementation. While more work is required to improve the framework’s ease-of-use and the speed of verification, the results show that this approach to hybrid verification is feasible.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.595236
Depositing User: Jason S. Reich
Date Deposited: 07 Apr 2014 13:05
Last Modified: 08 Sep 2016 13:30
URI: http://etheses.whiterose.ac.uk/id/eprint/5650

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)