Validating Formal Semantics by Property-Based Cross-Testing
Péter Bereczky, Dániel Horpácsi, Judit Köszegi, Soma Szeier, Simon Thompson · 2020
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?