<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Aptos;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:12.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">6th International Workshop on Formal Methods for Blockchains - First Call for Papers<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffmbc.gitlab.io%2F2025&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104750929%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=o%2FBU9kZH1sD0gUIaAMpz%2FdP%2BfB561moHRPiJfaODGK4%3D&reserved=0" originalSrc="https://fmbc.gitlab.io/2025" shash="DrPwG2vaI6GiIDBn04tXFtwkv3ple021wEvMZIn2GpRHTyEGY4cvAs619NwhQoUCpNSg8RHrQR/7a8Du3xQJAV386GXR16dzJG0cv5cYEfnchSkkc88MdnASEyQP8YqZBPYR5HfAVPXtPqJZoWLVMHmSAC3Wh22iWQwcWRZnPXM=">https://fmbc.gitlab.io/2025</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">May 04, 2025, Hamilton, ON, Canada<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Co-located with the European joint conferences on theory and practice of software (ETAPS 2025)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.etaps.org%2F2025%2F&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104750929%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=qcHK7hHmbnw0Ubh4FWVxhHXqaUsI%2BaymyCKe5LO9kDA%3D&reserved=0" originalSrc="https://www.etaps.org/2025/" shash="EBdb3zx6+hNYvhzbo5FYMDT7Rpc9+pFvYE2sy6gq3pfB4mTy+C8qs7i66lxQ/e5f6IgwwyINLpMgJtKdfbKhW54i+tOUjZUxvL39uiq0OGgJNpT88LsFLmedjZSf/m2JXexZV8QTMPWmEL+hyCoDaCVWWFojOcPtz5k50QG2WOQ=">https://www.etaps.org/2025/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">IMPORTANT DATES<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">Abstract submission: February 3rd, 2025<o:p></o:p></p>
<p class="MsoNormal">Full paper submission: February 10th, 2025<o:p></o:p></p>
<p class="MsoNormal">Notification: March 14th, 2025<o:p></o:p></p>
<p class="MsoNormal">Camera-ready: March 31st, 2025<o:p></o:p></p>
<p class="MsoNormal">Workshop: May 4th, 2025<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Deadlines are Anywhere on Earth:<o:p></o:p></p>
<p class="MsoNormal"><a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FAnywhere_on_Earth&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104907179%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=EKQOagbgj4BY3Pma5FSKTNfo%2BV3rUqM9TgEOJ9Wq4IM%3D&reserved=0" originalSrc="https://en.wikipedia.org/wiki/Anywhere_on_Earth" shash="VsgRRaJ0RNK1obIK7F7LdNpnFe8XPBDNN0y0zyzoK/XzkhF6iREZeJio3PaETz29soa4UAwEm7XHsEJSGAiYpf7kI2SDzBVilWQ7xbIuwfWyhKWOIcdNF2/gbAbpvt30EdMbPqvgj3po4voGgKMwHXAjoq4j+aZ0sAsEaSoJujw=">https://en.wikipedia.org/wiki/Anywhere_on_Earth</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">TOPICS OF INTEREST<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Blockchain is a novel technology to store data in a decentralized way.<o:p></o:p></p>
<p class="MsoNormal">Although the technology was originally invented to enable cryptocurrencies, it quickly found applications in several other domains.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are<o:p></o:p></p>
<p class="MsoNormal">stored in the blockchain and that run on the network. They can interact with the ledger’s data and update its state.<o:p></o:p></p>
<p class="MsoNormal">These scripts can express the logic of possibly complex contracts between users of the blockchain. Thus, Smart Contracts can facilitate<o:p></o:p></p>
<p class="MsoNormal">the economic activity of blockchain participants.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Since blockchains are often used to store financial transactions, bugs may result in huge economic losses and thus it is now of utmost<o:p></o:p></p>
<p class="MsoNormal">importance to have strong guarantees of the behaviour of blockchain software. These guarantees can be brought by using Formal Methods.<o:p></o:p></p>
<p class="MsoNormal">Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools is relevant:<o:p></o:p></p>
<p class="MsoNormal">consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to<o:p></o:p></p>
<p class="MsoNormal">write smart contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">This workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology.<o:p></o:p></p>
<p class="MsoNormal">Topics include, but are not limited to:<o:p></o:p></p>
<p class="MsoNormal">* Formal models of Blockchain applications or concepts<o:p></o:p></p>
<p class="MsoNormal">* Formal methods for consensus protocols<o:p></o:p></p>
<p class="MsoNormal">* Formal methods for Blockchain-specific cryptographic primitives or protocols<o:p></o:p></p>
<p class="MsoNormal">* Design and implementation of Smart Contract languages<o:p></o:p></p>
<p class="MsoNormal">* Verification of Smart Contracts<o:p></o:p></p>
<p class="MsoNormal">* Zero-knowledge proof and its applications in a blockchain setting<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal">SUBMISSION<o:p></o:p></p>
<p class="MsoNormal">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Submit original manuscripts (not published or considered elsewhere) with a page limit of 12 pages for full papers and 6 pages for short and tool papers<o:p></o:p></p>
<p class="MsoNormal">(excluding bibliography and short appendix of up to 5 additional pages).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Alternatively you may also submit an extended abstract of up to 3 pages (including bibliography) summarizing your ongoing work in the area of<o:p></o:p></p>
<p class="MsoNormal">formal methods and blockchain. Authors of selected extended-abstracts are invited to give a short lightning talk. Extended abstracts will not occur in<o:p></o:p></p>
<p class="MsoNormal">the workshop proceedings.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Submission link: <a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair.org%2Fconferences%2F%3Fconf%3Dfmbc2025&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104907179%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=c2zOq0IXxDn7XPnyPKRfQ48Irt8%2B7Y%2Bw3bZfd82DajU%3D&reserved=0" originalSrc="https://easychair.org/conferences/?conf=fmbc2025" shash="xdcW55qFx5DoWCW5oRR3nZeS0vTLQENyLMQfYdFEln3ozpO/Y4is75SI21ZiZrBBjTKyYUKxqOcahwry1MkRMfRohVlQfLN3A8ptRHYOoo24r8cWQLt7WQ4GT74l3OEhErHprALHmOsjn3ogDAehQSvogseok4WKZzDl5YVFwNo=">
https://easychair.org/conferences/?conf=fmbc2025</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Authors are encouraged to use LaTeX and prepare their submissions according to the instructions and styling guides for OASIcs provided by Dagstuhl.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Instructions for authors:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fsubmission.dagstuhl.de%2Fdocumentation%2Fauthors%23oasics&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104907179%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=%2B8f53fio38Qd7gQOdvEA1DOcBzO7nq9EqZehOCXJx6I%3D&reserved=0" originalSrc="https://submission.dagstuhl.de/documentation/authors#oasics" shash="ssiWQlq/EKCqLRzUQhsX4YDvVARuJLLr0xGAnIt1EUUq84002uluAVI+CnBB1VgFbKiYZkXQfPZCVi9rB+2U7PPMkG3IpLAzL7JwYoBSWme9KwKeNnTeaOG5pSLc0llvSA6a7jNbl372XsHJ29H+k1QzTtE36lcpziwoD1imNrE=">https://submission.dagstuhl.de/documentation/authors#oasics</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">At least one author of an accepted paper is expected to present the paper at the workshop as a registered participant.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal">PROCEEDINGS<o:p></o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">All submissions will be peer-reviewed by at least three members of the program committee for quality and relevance.<o:p></o:p></p>
<p class="MsoNormal">Accepted regular papers (full, short, and tool papers) will be included in the workshop proceeding, which will be published as a volume of the<o:p></o:p></p>
<p class="MsoNormal">OpenAccess Series in Informatics (OASIcs) by Dagstuhl.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal">PROGRAM COMMITTEE<o:p></o:p></p>
<p class="MsoNormal">--------------------------------<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">PC CO-CHAIRS<o:p></o:p></p>
<p class="MsoNormal">* Diego Marmsoler (University of Exeter, UK) (<a href="mailto:D.Marmsoler@exeter.ac.uk">D.Marmsoler@exeter.ac.uk</a>)<o:p></o:p></p>
<p class="MsoNormal">* Meng Xu (University of Waterloo, Canada) (<a href="mailto:meng.xu.cs@uwaterloo.ca">meng.xu.cs@uwaterloo.ca</a>)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">PC MEMBERS<o:p></o:p></p>
<p class="MsoNormal">* Massimo Bartoletti (University of Cagliari)<o:p></o:p></p>
<p class="MsoNormal">* Bernhard Beckert (Karlsruhe Institute of Technology)<o:p></o:p></p>
<p class="MsoNormal">* Franck Cassez (Mantle)<o:p></o:p></p>
<p class="MsoNormal">* Denisa Diaconescu (University of Bucharest)<o:p></o:p></p>
<p class="MsoNormal">* Maurice Herlihy (Brown University)<o:p></o:p></p>
<p class="MsoNormal">* Sebastian Holler (Max Planck Institute for Security and Privacy)<o:p></o:p></p>
<p class="MsoNormal">* Enrico Lipparini (University of Genoa)<o:p></o:p></p>
<p class="MsoNormal">* Fan Long (University of Toronto)<o:p></o:p></p>
<p class="MsoNormal">* Orestis Melkonian (Input Output (IOG))<o:p></o:p></p>
<p class="MsoNormal">* Baoluo Meng (GE Aerospace Research)<o:p></o:p></p>
<p class="MsoNormal">* Burcu Kulahcioglu Ozkan (Delft University of Technology)<o:p></o:p></p>
<p class="MsoNormal">* Gordon Pace (University of Malta)<o:p></o:p></p>
<p class="MsoNormal">* Vincent Rahli (University of Birmingham)<o:p></o:p></p>
<p class="MsoNormal">* Sophie Rain (TU Wien)<o:p></o:p></p>
<p class="MsoNormal">* Augusto Sampaio (Federal university of Pernambuco)<o:p></o:p></p>
<p class="MsoNormal">* Derek Sorensen (Certora)<o:p></o:p></p>
<p class="MsoNormal">* Bas Spitters (Aarhus University)<o:p></o:p></p>
<p class="MsoNormal">* Meng Sun (Peking University)<o:p></o:p></p>
<p class="MsoNormal">* Mark Utting (The University of Queensland)<o:p></o:p></p>
<p class="MsoNormal">* Adele Veschetti (TU Darmstadt)<o:p></o:p></p>
<p class="MsoNormal">* Christoph Weidenbach (Max Planck Institute for Informatics)<o:p></o:p></p>
<p class="MsoNormal">* Teng Zhang (Aptos Labs)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:gray;mso-ligatures:none;mso-fareast-language:EN-GB">Diego Marmsoler</span></b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">
<br>
</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:gray;mso-ligatures:none;mso-fareast-language:EN-GB">Lecturer (Education and Research), Computer Science
<br>
University of Exeter, Innovation 1, Room 10<o:p></o:p></span></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:gray;mso-ligatures:none;mso-fareast-language:EN-GB">www:
<a href="https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.marmsoler.com%2F&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104907179%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=M3s26jJkazPEdd2VCHFB7BvIDAb1z6ohYz290gtauTE%3D&reserved=0" originalSrc="http://www.marmsoler.com/" shash="zb+QHghUrU1BKPSrN54eX/J9YrEEMO2m0H1TzbHCBh/1sDks/3gKn5mVe26LZpsmx9miXdaDRB3Kv68bRThsUkJQ6LC/PwL2qg0sV3SDsL1q86ezHNPzDfDBUcC88uQdoP1u1+uMEWS6YEgEDBktOsOaC9VvhmXGhIgfGlJUFDA=">marmsoler.com</a><br>
Twitter: <a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Ftwitter.com%2FDiegoMarmsoler&data=05%7C02%7Com-announce%40openmath.org%7Cb522649e238f489b0fc608dd160c072e%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638690963104907179%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C80000%7C%7C%7C&sdata=uYEEdCmCAKctq%2FLuA1brjsS7Xh480XceeQDQxhPMh0Y%3D&reserved=0" originalSrc="https://twitter.com/DiegoMarmsoler" shash="TJHxC4kl8q3yk+UZMzFfYQY1IZh6t4BFpnubUgATaTcwAUzdaR4GwqFfkQA8bhfY+dazebpfifdTb6wYZJUd/aPe+7bC6Qmhe1bUEbNCYSt1mfi2iwV/kzkZG9CgJNAQBPE0SLQCWp7r40se769PslfIS33Pcx7jB3PELPJNDDk=">@DiegoMarmsoler</a><o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>