RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer
Conformance testing asks whether an implementation agrees with its specification. When the specification is expressed in prose, one established approach is to mechanize it as an executable specification. This executable then serves as the oracle, and an input on which an implementation disagrees with it is a potential...