Technical Report: DCC-2013-06

Verifying a Simple Compiler Using Property-based Random Testing

Pedro Vasconcelos

DCC-FC & LIACC, Universidade do Porto
e-mail: pbv@dcc.fc.up.pt
April 2013

Abstract

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.