Technical Report: DCC-2013-06

Verifying a Simple Compiler Using Property-based Random Testing

Pedro Vasconcelos

DCC-FC & LIACC, Universidade do Porto
April 2013


This paper reports on the use of the Haskell \emph{QuickCheck} library for testing the correctness of a simple functional compiler and abstract machine. We use QuickCheck to express the correctness of the abstract machine against a denotational semantics, to generate well-formed test programs and to automatically shrink counterexamples obtained when a test fails.