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 JanDisplayed time zone: Belfast change
Sat 19 Jan
Displayed time zone: Belfast change
11:15 - 12:30 | |||
11:15 25mTalk | Towards Mechanising Probabilistic Properties of a Blockchain CoqPL Kiran Gopinathan University College London, Ilya Sergey Yale-NUS College and National University of Singapore File Attached | ||
11:40 25mTalk | Verifying Finality for Blockchain Systems CoqPL Karl Palmskog University of Texas at Austin, Milos Gligoric University of Texas at Austin, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign File Attached | ||
12:05 25mTalk | WIP: Formalizing the Concordium Consensus Protocol in Coq CoqPL Thomas Dinsdale-Young , Bas Spitters Aarhus University, Søren Eller Thomsen Aarhus University, Daniel Tschudi Aarhus University File Attached |