Search Results

Documents authored by Marmsoler, Diego

Document
Complete Volume
DOI: 10.4230/OASIcs.FMBC.2025
OASIcs, Volume 129, FMBC 2025, Complete Volume

Authors: Diego Marmsoler and Meng Xu

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
OASIcs, Volume 129, FMBC 2025, Complete Volume
Cite as

6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 1-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{marmsoler_et_al:OASIcs.FMBC.2025,
  title =	{{OASIcs, Volume 129, FMBC 2025, Complete Volume}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{1--222},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025},
  URN =		{urn:nbn:de:0030-drops-231256},
  doi =		{10.4230/OASIcs.FMBC.2025},
  annote =	{Keywords: OASIcs, Volume 129, FMBC 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.FMBC.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Diego Marmsoler and Meng Xu

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{marmsoler_et_al:OASIcs.FMBC.2025.0,
  author =	{Marmsoler, Diego and Xu, Meng},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{0:i--0:xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.0},
  URN =		{urn:nbn:de:0030-drops-230831},
  doi =		{10.4230/OASIcs.FMBC.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Tool Paper
DOI: 10.4230/OASIcs.FMBC.2025.12
Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts (Tool Paper)

Authors: Asad Ahmed and Diego Marmsoler

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Smart contracts are an important innovation in Blockchain which allow to automate financial transactions. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars' worth of transactions. Thus, bugs in smart contracts may lead to high financial losses and it is important to get them right before deploying them to the Blockchain. To address this problem we developed Isabelle/Solidity, a tool for the verification of smart contracts in Isabelle. The tool is implemented as a definitional extension for the Isabelle proof assistant and thus complements existing tools in this area which are mostly based on axiomatic approaches. In this paper we describe Isabelle/Solidity and demonstrate it by verifying a casino contract from the VerifyThis long term verification challenge.
Cite as

Asad Ahmed and Diego Marmsoler. Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts (Tool Paper). In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 12:1-12:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:OASIcs.FMBC.2025.12,
  author =	{Ahmed, Asad and Marmsoler, Diego},
  title =	{{Isabelle/Solidity: A Tool for the Verification of Solidity Smart Contracts}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{12:1--12:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.12},
  URN =		{urn:nbn:de:0030-drops-230393},
  doi =		{10.4230/OASIcs.FMBC.2025.12},
  annote =	{Keywords: Program Verification, Smart Contracts, Isabelle, Solidity}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.FMBC.2024
OASIcs, Volume 118, FMBC 2024, Complete Volume

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
OASIcs, Volume 118, FMBC 2024, Complete Volume
Cite as

5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 1-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{bernardo_et_al:OASIcs.FMBC.2024,
  title =	{{OASIcs, Volume 118, FMBC 2024, Complete Volume}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{1--164},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  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.2024},
  URN =		{urn:nbn:de:0030-drops-198642},
  doi =		{10.4230/OASIcs.FMBC.2024},
  annote =	{Keywords: OASIcs, Volume 118, FMBC 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.FMBC.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bernardo_et_al:OASIcs.FMBC.2024.0,
  author =	{Bernardo, Bruno and Marmsoler, Diego},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{0:i--0:xii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  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.2024.0},
  URN =		{urn:nbn:de:0030-drops-198659},
  doi =		{10.4230/OASIcs.FMBC.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.4
Towards Mechanised Consensus in Isabelle

Authors: Elliot Jones and Diego Marmsoler

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is in majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.
Cite as

Elliot Jones and Diego Marmsoler. Towards Mechanised Consensus in Isabelle. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jones_et_al:OASIcs.FMBC.2024.4,
  author =	{Jones, Elliot and Marmsoler, Diego},
  title =	{{Towards Mechanised Consensus in Isabelle}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{4:1--4:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  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.2024.4},
  URN =		{urn:nbn:de:0030-drops-198692},
  doi =		{10.4230/OASIcs.FMBC.2024.4},
  annote =	{Keywords: Formal Methods, Blockchain, Isabelle/HOL, Consensus, Verification, Theorem Provers}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.FMBC.2021
OASIcs, Volume 95, FMBC 2021, Complete Volume

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
OASIcs, Volume 95, FMBC 2021, Complete Volume
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
Front Matter
DOI: 10.4230/OASIcs.FMBC.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.FMBC.2020
OASIcs, Volume 84, FMBC 2020, Complete Volume

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract
OASIcs, Volume 84, FMBC 2020, Complete Volume
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
Front Matter
DOI: 10.4230/OASIcs.FMBC.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact