<h2>OASIcs, Volume 118, FMBC 2024</h2>
<ul>
<li>
<span class="authors">Bruno Bernardo and Diego Marmsoler</span>
<span class="title">OASIcs, Volume 118, FMBC 2024, Complete Volume</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024">10.4230/OASIcs.FMBC.2024</a>
</li>
<li>
<span class="authors">Bruno Bernardo and Diego Marmsoler</span>
<span class="title">Front Matter, Table of Contents, Preface, Conference Organization</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.0">10.4230/OASIcs.FMBC.2024.0</a>
</li>
<li>
<span class="authors">Franck Cassez</span>
<span class="title">Deductive Verification of Smart Contracts (Invited Talk)</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.1">10.4230/OASIcs.FMBC.2024.1</a>
</li>
<li>
<span class="authors">Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell</span>
<span class="title">Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.2">10.4230/OASIcs.FMBC.2024.2</a>
</li>
<li>
<span class="authors">M. Praveen, Raghavendra Ramesh, and Isaac Doidge</span>
<span class="title">Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.3">10.4230/OASIcs.FMBC.2024.3</a>
</li>
<li>
<span class="authors">Elliot Jones and Diego Marmsoler</span>
<span class="title">Towards Mechanised Consensus in Isabelle</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.4">10.4230/OASIcs.FMBC.2024.4</a>
</li>
<li>
<span class="authors">Daniele Pusceddu and Massimo Bartoletti</span>
<span class="title">Formalizing Automated Market Makers in the Lean 4 Theorem Prover</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.5">10.4230/OASIcs.FMBC.2024.5</a>
</li>
<li>
<span class="authors">Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, and Franco Sainas</span>
<span class="title">Towards Benchmarking of Solidity Verification Tools</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.6">10.4230/OASIcs.FMBC.2024.6</a>
</li>
<li>
<span class="authors">Derek Sorensen</span>
<span class="title">Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.7">10.4230/OASIcs.FMBC.2024.7</a>
</li>
<li>
<span class="authors">Jonas Schiffl and Bernhard Beckert</span>
<span class="title">A Practical Notion of Liveness in Smart Contract Applications</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.8">10.4230/OASIcs.FMBC.2024.8</a>
</li>
<li>
<span class="authors">Junkil Park, Teng Zhang, Wolfgang Grieskamp, Meng Xu, Gerardo Di Giacomo, Kundu Chen, Yi Lu, and Robert Chen</span>
<span class="title">Securing Aptos Framework with Formal Verification</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.9">10.4230/OASIcs.FMBC.2024.9</a>
</li>
<li>
<span class="authors">Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu</span>
<span class="title">Structured Contracts in the EUTxO Ledger Model</span>
<a class="doi" href="https://doi.org/10.4230/OASIcs.FMBC.2024.10">10.4230/OASIcs.FMBC.2024.10</a>
</li>
</ul>
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