• Java 1.4: by Bogdanas etal [POPL’15] – 800+ program test suite that covers the semantics • JavaScript ES5: by Park etal [PLDI’15] – Passes existing conformance test suite (2872 programs) – Found (confirmed) bugs in Chrome, IE, Firefox, Safari • C11: Ellison etal [POPL’12, PLDI’15] – 192 different types of undefined behavior – 10,000+ program tests (gcc torture tests, obfuscated C, …) – Commercialized by startup (Runtime Verification, Inc.) … + EVM, Solidity, IELE, Plutus, Vyper [????’18-’19] 13