Benedikt F. H. Becker, Claude Marché: Ghost Code in Action: Automated Verification of a Symbolic Interpreter. VSTTE 2019: 107-123