POPL 2019 (series) / CoqPL 2019 (series) / The Fifth International Workshop on Coq for Programming Languages /
Towards Mechanising Probabilistic Properties of a Blockchain
We present our progress on the formalisation and mechanisation of a probabilistic model of a blockchain consensus protocol in Coq, taking steps towards the formal verification of its security properties, stated in terms of probabilities, in an adversarial environment.
Presentation Slides (probchain_coqpl_presentation.pdf) | 576KiB |
Abstract (coqpl19-final13.pdf) | 583KiB |
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sat 19 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
11:15 - 11:40 Talk | Towards Mechanising Probabilistic Properties of a Blockchain CoqPL Kiran GopinathanUniversity College London, Ilya SergeyYale-NUS College and National University of Singapore File Attached | ||
11:40 - 12:05 Talk | Verifying Finality for Blockchain Systems CoqPL Karl PalmskogUniversity of Texas at Austin, Milos GligoricUniversity of Texas at Austin, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign File Attached | ||
12:05 - 12:30 Talk | WIP: Formalizing the Concordium Consensus Protocol in Coq CoqPL Thomas Dinsdale-Young, Bas SpittersAarhus University, Søren Eller ThomsenAarhus University, Daniel TschudiAarhus University File Attached |