End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract[C] COMPUTER AIDED VERIFICATION (CAV 2020), PT I 2020(12224) Park, Daejun Zhang, Yi Rosu, Grigore