Property-based testing of the meta-theory of abstract machines: An experience report

Contrary to Dijkstra's diktat, testing, and more in general validation has found an increasing niche in formal verification, prior or even in alternative to theorem proving. In particular, property-based testing (PBT) is quite effective in mechanized meta-theory of programming languages, where theorems have shallow but tedious proofs that may go wrong for fairly banal mistakes. In this report, we abandon the comfort of high-level object languages and address the validation of abstract machines and typed assembly languages. We concentrate on Appel et al.'s list-machine benchmark [ADL12], which we tackle with αCheck, the simple model-checker on top of the nominal logic programming αProlog. We uncover one major bug in the published version of the paper plus several typos and ambiguities thereof. This is particularly striking, as the paper is accompanied by two full formalizations, in Coq and Twelf. Finally, we carry out some mutation testing on the given model, to asses the trade-off between exhaustive and randomized data generation, using for the latter the PBT library FSCheck for F#. Spoiler alert: aProlog performs better. © Copyright 2018 for the individual papers by the papers' authors.