EthBMC July, 2020 A bounded model checker for smart contracts, that can steal money. Published at USENIX Security 2020