Mechanized Formal Model of Bitcoin's Blockchain Validation Procedures. - Kristijan Rupic; Lovro Rozic; Ante Derek (FMBC@CAV, 2020)