Kristijan Rupić (kristijan.rupic at fer.hr), Lovro Rožić (lorozic33 at gmail.com), and Ante Đerek (ante.derek at fer.hr)
Faculty of Electrical Engineering and Computing, University of Zagreb
This is the Coq artifact of our paper "Mechanized Formal Model of Bitcoin's Blockchain Validation Procedures" submitted to FMBC 2020.
Run coq_makefile -f _CoqProject -o makefile and then make.
Utils.v has to be compiled before Bitcoin.v works. Checked with Coq version 8.10.2.