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

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.