OASIcs, Volume 95
FMBC 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference)
Editors: Bruno Bernardo and Diego Marmsoler
OASIcs, Volume 84
FMBC 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference)
Editors: Bruno Bernardo and Diego Marmsoler
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@Proceedings{bernardo_et_al:OASIcs.FMBC.2021, title = {{OASIcs, Volume 95, FMBC 2021, Complete Volume}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {1--68}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021}, URN = {urn:nbn:de:0030-drops-154239}, doi = {10.4230/OASIcs.FMBC.2021}, annote = {Keywords: OASIcs, Volume 95, FMBC 2021, Complete Volume} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{bernardo_et_al:OASIcs.FMBC.2021.0, author = {Bernardo, Bruno and Marmsoler, Diego}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {0:i--0:xii}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.0}, URN = {urn:nbn:de:0030-drops-154246}, doi = {10.4230/OASIcs.FMBC.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun. Towards Verified Price Oracles for Decentralized Exchange Protocols. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{dave_et_al:OASIcs.FMBC.2021.1, author = {Dave, Kinnari and Sj\"{o}berg, Vilhelm and Sun, Xinyuan}, title = {{Towards Verified Price Oracles for Decentralized Exchange Protocols}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {1:1--1:14}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.1}, URN = {urn:nbn:de:0030-drops-154254}, doi = {10.4230/OASIcs.FMBC.2021.1}, annote = {Keywords: Smart Contract Verification, Interactive Theorem Proving, Blockchain, Decentralized Finance} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Murdoch J. Gabbay, Arvid Jakobsson, and Kristina Sojakova. Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{gabbay_et_al:OASIcs.FMBC.2021.2, author = {Gabbay, Murdoch J. and Jakobsson, Arvid and Sojakova, Kristina}, title = {{Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {2:1--2:14}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.2}, URN = {urn:nbn:de:0030-drops-154267}, doi = {10.4230/OASIcs.FMBC.2021.2}, annote = {Keywords: Distributed ledger, smart contracts, Coq, formal verification, blockchain} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Daniel Britten, Vilhelm Sjöberg, and Steve Reeves. Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{britten_et_al:OASIcs.FMBC.2021.3, author = {Britten, Daniel and Sj\"{o}berg, Vilhelm and Reeves, Steve}, title = {{Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {3:1--3:8}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.3}, URN = {urn:nbn:de:0030-drops-154272}, doi = {10.4230/OASIcs.FMBC.2021.3}, annote = {Keywords: smart contracts, formal methods, blockchain} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally Documenting Tenderbake (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{conchon_et_al:OASIcs.FMBC.2021.4, author = {Conchon, Sylvain and Korneva, Alexandrina and Bozman, \c{C}agdas and Iguernlala, Mohamed and Mebsout, Alain}, title = {{Formally Documenting Tenderbake}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {4:1--4:9}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.4}, URN = {urn:nbn:de:0030-drops-154281}, doi = {10.4230/OASIcs.FMBC.2021.4}, annote = {Keywords: Consensus algorithm, Tezos blockchain, TLA+} }
Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{doan_et_al:OASIcs.FMBC.2021.5, author = {Doan, Thi Thu Ha and Thiemann, Peter}, title = {{Towards Contract Modules for the Tezos Blockchain}}, booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)}, pages = {5:1--5:9}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-209-9}, ISSN = {2190-6807}, year = {2021}, volume = {95}, 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.2021.5}, URN = {urn:nbn:de:0030-drops-154294}, doi = {10.4230/OASIcs.FMBC.2021.5}, annote = {Keywords: contract API, modules, static checking} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 1-136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie. Formal Specification and Verification of Solidity Contracts with Events (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Maria A. Schett and Julian Nagele. Populating the Peephole Optimizer of a Smart Contract Compiler. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
João Santos Reis, Paul Crocker, and Simão Melo de Sousa. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@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} }
Feedback for Dagstuhl Publishing