FMBC 2020 July 20-21, 2020, Los Angeles, California, USA (Virtual Conference)

2nd Workshop on Formal Methods for Blockchains (FMBC 2020)



Bruno Bernardo and Diego Marmsoler (Eds.)
ISBN 978-3-95977-169-6, OASICS Vol. 84 ISSN 2190-6807
Additional Information
License
Conference Website
Complete volume (PDF, 5 MB)
Search Publication Server

Authors
  • Bernardo, Bruno
  • Boss, Ramon
  • Boyd, Colin
  • Braithwaite, Sean
  • Brünnler, Kai
  • Buchman, Ethan
  • Ciocarlie, Gabriela
  • Crocker, Paul
  • Derek, Ante
  • Dodds, Mike
  • Doukmak, Anna
  • Gjøsteen, Kristian
  • Hajdu, Ákos
  • Jovanović, Dejan
  • Kammüller, Florian
  • Konnov, Igor
  • Lochbihler, Andreas
  • Losa, Giuliano
  • Marić, Ognjen
  • Marmsoler, Diego
  • Melo de Sousa, Simão
  • Milosevic, Zarko
  • Nagele, Julian
  • Nestmann, Uwe
  • Rosu, Grigore
  • Rožić, Lovro
  • Rupić, Kristijan
  • Santos Reis, João
  • Schett, Maria A.
  • Stoilkovska, Ilina
  • Widder, Josef
  • Wu, Shuang
  • Zamfir, Anca
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Bernardo, Bruno ; Marmsoler, Diego

    Abstract | Document (540 KB) | BibTeX

    Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)
    Authors: Rosu, Grigore

    Abstract | Document (211 KB) | BibTeX

    Formal Specification and Verification of Solidity Contracts with Events (Short Paper)
    Authors: Hajdu, Ákos ; Jovanović, Dejan ; Ciocarlie, Gabriela

    Abstract | Document (454 KB) | BibTeX

    Populating the Peephole Optimizer of a Smart Contract Compiler
    Authors: Schett, Maria A. ; Nagele, Julian

    Abstract | Document (593 KB) | BibTeX

    Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
    Authors: Santos Reis, João ; Crocker, Paul ; Melo de Sousa, Simão

    Abstract | Document (447 KB) | BibTeX

    A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract
    Authors: Boyd, Colin ; Gjøsteen, Kristian ; Wu, Shuang

    Abstract | Document (446 KB) | BibTeX

    Authenticated Data Structures as Functors in Isabelle/HOL
    Authors: Lochbihler, Andreas ; Marić, Ognjen

    Abstract | Document (433 KB) | BibTeX

    Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures
    Authors: Rupić, Kristijan ; Rožić, Lovro ; Derek, Ante

    Abstract | Document (447 KB) | BibTeX

    Towards Verifying the Bitcoin-S Library (Short Paper)
    Authors: Boss, Ramon ; Brünnler, Kai ; Doukmak, Anna

    Abstract | Document (399 KB) | BibTeX

    On the Formal Verification of the Stellar Consensus Protocol
    Authors: Losa, Giuliano ; Dodds, Mike

    Abstract | Document (398 KB) | BibTeX

    Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
    Authors: Braithwaite, Sean ; Buchman, Ethan ; Konnov, Igor ; Milosevic, Zarko ; Stoilkovska, Ilina ; Widder, Josef ; Zamfir, Anca

    Abstract | Document (522 KB) | BibTeX

    Inter-Blockchain Protocols with the Isabelle Infrastructure Framework
    Authors: Kammüller, Florian ; Nestmann, Uwe

    Abstract | Document (598 KB) | BibTeX

    		  



    DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI