@Proceedings{bernardo_et_al:OASIcs.FMBC.2020,
title = {{OASIcs, Volume 84, FMBC 2020, Complete Volume}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {1--136},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020},
URN = {urn:nbn:de:0030-drops-134121},
doi = {10.4230/OASIcs.FMBC.2020},
annote = {Keywords: OASIcs, Volume 84, FMBC 2020, Complete Volume}
}
@InProceedings{bernardo_et_al:OASIcs.FMBC.2020.0,
author = {Bernardo, Bruno and Marmsoler, Diego},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {0:i--0:xii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.0},
URN = {urn:nbn:de:0030-drops-134137},
doi = {10.4230/OASIcs.FMBC.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{rosu:OASIcs.FMBC.2020.1,
author = {Rosu, Grigore},
title = {{Formal Design, Implementation and Verification of Blockchain Languages Using K}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {1:1--1:1},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.1},
URN = {urn:nbn:de:0030-drops-134141},
doi = {10.4230/OASIcs.FMBC.2020.1},
annote = {Keywords: Blockchain, K Framework}
}
@InProceedings{hajdu_et_al:OASIcs.FMBC.2020.2,
author = {Hajdu, \'{A}kos and Jovanovi\'{c}, Dejan and Ciocarlie, Gabriela},
title = {{Formal Specification and Verification of Solidity Contracts with Events}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {2:1--2:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.2},
URN = {urn:nbn:de:0030-drops-134153},
doi = {10.4230/OASIcs.FMBC.2020.2},
annote = {Keywords: Smart contracts, Solidity, events, specification, verification}
}
@InProceedings{schett_et_al:OASIcs.FMBC.2020.3,
author = {Schett, Maria A. and Nagele, Julian},
title = {{Populating the Peephole Optimizer of a Smart Contract Compiler}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {3:1--3:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.3},
URN = {urn:nbn:de:0030-drops-134169},
doi = {10.4230/OASIcs.FMBC.2020.3},
annote = {Keywords: Compiler Optimizations, Constraint Solving, Ethereum Bytecode}
}
@InProceedings{santosreis_et_al:OASIcs.FMBC.2020.4,
author = {Santos Reis, Jo\~{a}o and Crocker, Paul and Melo de Sousa, Sim\~{a}o},
title = {{Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {4:1--4:12},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.4},
URN = {urn:nbn:de:0030-drops-134176},
doi = {10.4230/OASIcs.FMBC.2020.4},
annote = {Keywords: Intermediate representation, Static analysis, Tezos blockchain, Michelson}
}
@InProceedings{boyd_et_al:OASIcs.FMBC.2020.5,
author = {Boyd, Colin and Gj{\o}steen, Kristian and Wu, Shuang},
title = {{A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {5:1--5:13},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.5},
URN = {urn:nbn:de:0030-drops-134187},
doi = {10.4230/OASIcs.FMBC.2020.5},
annote = {Keywords: Blockchain model, Tamarin, Hash time lock contract, Formal verification}
}
@InProceedings{lochbihler_et_al:OASIcs.FMBC.2020.6,
author = {Lochbihler, Andreas and Mari\'{c}, Ognjen},
title = {{Authenticated Data Structures as Functors in Isabelle/HOL}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {6:1--6:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.6},
URN = {urn:nbn:de:0030-drops-134196},
doi = {10.4230/OASIcs.FMBC.2020.6},
annote = {Keywords: Merkle tree, functor, distributed ledger, datatypes, higher-order logic}
}
@InProceedings{rupic_et_al:OASIcs.FMBC.2020.7,
author = {Rupi\'{c}, Kristijan and Ro\v{z}i\'{c}, Lovro and Derek, Ante},
title = {{Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {7:1--7:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.7},
URN = {urn:nbn:de:0030-drops-134209},
doi = {10.4230/OASIcs.FMBC.2020.7},
annote = {Keywords: blockchain, Bitcoin, program verification, Coq}
}
@InProceedings{boss_et_al:OASIcs.FMBC.2020.8,
author = {Boss, Ramon and Br\"{u}nnler, Kai and Doukmak, Anna},
title = {{Towards Verifying the Bitcoin-S Library}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {8:1--8:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.8},
URN = {urn:nbn:de:0030-drops-134212},
doi = {10.4230/OASIcs.FMBC.2020.8},
annote = {Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}
@InProceedings{losa_et_al:OASIcs.FMBC.2020.9,
author = {Losa, Giuliano and Dodds, Mike},
title = {{On the Formal Verification of the Stellar Consensus Protocol}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {9:1--9:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.9},
URN = {urn:nbn:de:0030-drops-134226},
doi = {10.4230/OASIcs.FMBC.2020.9},
annote = {Keywords: Consensus, Blockchains, First-Order Logic, Stellar, Ivy Prover, Decidability}
}
@InProceedings{braithwaite_et_al:OASIcs.FMBC.2020.10,
author = {Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca},
title = {{Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {10:1--10:8},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.10},
URN = {urn:nbn:de:0030-drops-134238},
doi = {10.4230/OASIcs.FMBC.2020.10},
annote = {Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking}
}
@InProceedings{kammuller_et_al:OASIcs.FMBC.2020.11,
author = {Kamm\"{u}ller, Florian and Nestmann, Uwe},
title = {{Inter-Blockchain Protocols with the Isabelle Infrastructure Framework}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {11:1--11:12},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.11},
URN = {urn:nbn:de:0030-drops-134249},
doi = {10.4230/OASIcs.FMBC.2020.11},
annote = {Keywords: Blockchain, smart contracts, interactive theorem proving, inter-blockchain protocols}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing