@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}
}
@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}
}
@InProceedings{cassez:OASIcs.FMBC.2024.1,
  author =	{Cassez, Franck},
  title =	{{Deductive Verification of Smart Contracts}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{1:1--1:1},
  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.1},
  URN =		{urn:nbn:de:0030-drops-198664},
  doi =		{10.4230/OASIcs.FMBC.2024.1},
  annote =	{Keywords: Smart Contracts, Deductive Verification}
}
@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  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.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
@InProceedings{praveen_et_al:OASIcs.FMBC.2024.3,
  author =	{Praveen, M. and Ramesh, Raghavendra and Doidge, Isaac},
  title =	{{Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{3:1--3:16},
  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.3},
  URN =		{urn:nbn:de:0030-drops-198688},
  doi =		{10.4230/OASIcs.FMBC.2024.3},
  annote =	{Keywords: Blockchain consensus, Safety, Formal verification}
}
@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}
}
@InProceedings{pusceddu_et_al:OASIcs.FMBC.2024.5,
  author =	{Pusceddu, Daniele and Bartoletti, Massimo},
  title =	{{Formalizing Automated Market Makers in the Lean 4 Theorem Prover}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{5:1--5:13},
  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.5},
  URN =		{urn:nbn:de:0030-drops-198702},
  doi =		{10.4230/OASIcs.FMBC.2024.5},
  annote =	{Keywords: Smart contracts, Ethereum, Verification, Blockchain}
}
@InProceedings{bartoletti_et_al:OASIcs.FMBC.2024.6,
  author =	{Bartoletti, Massimo and Fioravanti, Fabio and Matricardi, Giulia and Pettinau, Roberto and Sainas, Franco},
  title =	{{Towards Benchmarking of Solidity Verification Tools}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{6:1--6:15},
  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.6},
  URN =		{urn:nbn:de:0030-drops-198719},
  doi =		{10.4230/OASIcs.FMBC.2024.6},
  annote =	{Keywords: Smart contracts, Ethereum, Verification, Blockchain}
}
@InProceedings{sorensen:OASIcs.FMBC.2024.7,
  author =	{Sorensen, Derek},
  title =	{{Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{7:1--7:14},
  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.7},
  URN =		{urn:nbn:de:0030-drops-198728},
  doi =		{10.4230/OASIcs.FMBC.2024.7},
  annote =	{Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgrades}
}
@InProceedings{schiffl_et_al:OASIcs.FMBC.2024.8,
  author =	{Schiffl, Jonas and Beckert, Bernhard},
  title =	{{A Practical Notion of Liveness in Smart Contract Applications}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{8:1--8:13},
  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.8},
  URN =		{urn:nbn:de:0030-drops-198732},
  doi =		{10.4230/OASIcs.FMBC.2024.8},
  annote =	{Keywords: Smart Contracts, Formal Verification, Security, Safety and Liveness}
}
@InProceedings{park_et_al:OASIcs.FMBC.2024.9,
  author =	{Park, Junkil and Zhang, Teng and Grieskamp, Wolfgang and Xu, Meng and Di Giacomo, Gerardo and Chen, Kundu and Lu, Yi and Chen, Robert},
  title =	{{Securing Aptos Framework with Formal Verification}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{9:1--9:16},
  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.9},
  URN =		{urn:nbn:de:0030-drops-198741},
  doi =		{10.4230/OASIcs.FMBC.2024.9},
  annote =	{Keywords: Formal verification, Smart contracts, Aptos Network, The Move language, The Move Prover}
}
@InProceedings{vinogradova_et_al:OASIcs.FMBC.2024.10,
  author =	{Vinogradova, Polina and Melkonian, Orestis and Wadler, Philip and Chakravarty, Manuel and Krijnen, Jacco and Jones, Michael Peyton and Chapman, James and Ferariu, Tudor},
  title =	{{Structured Contracts in the EUTxO Ledger Model}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{10:1--10:19},
  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.10},
  URN =		{urn:nbn:de:0030-drops-198757},
  doi =		{10.4230/OASIcs.FMBC.2024.10},
  annote =	{Keywords: blockchain, ledger, smart contract, formal verification, specification, transition systems, Agda, UTxO, EUTxO, small-step semantics}
}