Validating Formal Semantics by Property-Based Cross-Testing

To describe the behaviour of programs in a programming language we can define a formal semantics for the language, and formalise it in a proof assistant. From this semantics we can derive the behaviour of each particular program in the language. But there remains the question of validating the formal semantics: have we got the formalisation right?

Our approach is to use property-based cross-testing of formal semantics, which is based on the combination of a number of existing approaches to validation. In particular, we give a concrete implementation of our ideas for a set of formalisations of Erlang and Core Erlang. We describe the adjustments that need to be made to execute these seman- tics, then we present and evaluate property-based testing in the context of cross-checking semantics, including random program generation and counterexample shrinking.