<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<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;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin-top:0cm;
margin-right:0cm;
margin-bottom:8.0pt;
margin-left:0cm;
line-height:107%;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
{mso-style-priority:99;
mso-style-link:"Plain Text Char";
margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.PlainTextChar
{mso-style-name:"Plain Text Char";
mso-style-priority:99;
mso-style-link:"Plain Text";
font-family:"Calibri",sans-serif;
mso-ligatures:none;
mso-fareast-language:EN-GB;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
.MsoPapDefault
{mso-style-type:export-only;
margin-bottom:8.0pt;
line-height:107%;}
@page WordSection1
{size:595.3pt 841.9pt;
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="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoPlainText">[ Please distribute, apologies for multiple postings. ]<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">=========================================================================<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">5th International Workshop on Formal Methods for Blockchains - Second Call<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><a href="https://fmbc.gitlab.io/2024">https://fmbc.gitlab.io/2024</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">April 07, 2024, Luxembourg City, Luxembourg<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Co-located with the European joint conferences on theory and practice of software (ETAPS 2024)<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><a href="https://www.etaps.org/2024/">https://www.etaps.org/2024/</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">IMPORTANT DATES<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">Abstract submission: January 24, 2024<o:p></o:p></p>
<p class="MsoPlainText">Paper submission: January 31, 2024<o:p></o:p></p>
<p class="MsoPlainText">Notification: February 29, 2024<o:p></o:p></p>
<p class="MsoPlainText">Camera-ready: March 15, 2024<o:p></o:p></p>
<p class="MsoPlainText">Pre-Proceedings: March 31, 2024<o:p></o:p></p>
<p class="MsoPlainText">Workshop: April 07, 2024<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Deadlines are Anywhere on Earth:<o:p></o:p></p>
<p class="MsoPlainText"><a href="https://en.wikipedia.org/wiki/Anywhere_on_Earth">https://en.wikipedia.org/wiki/Anywhere_on_Earth</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">TOPICS OF INTEREST<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Blockchain is a novel technology to store data in a decentralized way.<o:p></o:p></p>
<p class="MsoPlainText">Although the technology was originally invented to enable cryptocurrencies, it quickly found applications in several other domains.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are</p>
<p class="MsoPlainText">stored in the blockchain and that run on the network. They can interact with the ledger’s data and update its state.</p>
<p class="MsoPlainText">These scripts can express the logic of possibly complex contracts between users of the blockchain. Thus, Smart Contracts can facilitate</p>
<p class="MsoPlainText">the economic activity of blockchain participants.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Since blockchains are often used to store financial transactions, bugs may result in huge economic losses and thus it is now of utmost</p>
<p class="MsoPlainText">importance to have strong guarantees of the behaviour of blockchain software. These guarantees can be brought by using Formal Methods.</p>
<p class="MsoPlainText">Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools is relevant:</p>
<p class="MsoPlainText">consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to</p>
<p class="MsoPlainText">write smart contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc.<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">This workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology.</p>
<p class="MsoPlainText">Topics include, but are not limited to:<o:p></o:p></p>
<p class="MsoPlainText">* Formal models of Blockchain applications or concepts<o:p></o:p></p>
<p class="MsoPlainText">* Formal methods for consensus protocols<o:p></o:p></p>
<p class="MsoPlainText">* Formal methods for Blockchain-specific cryptographic primitives or protocols<o:p></o:p></p>
<p class="MsoPlainText">* Design and implementation of Smart Contract languages<o:p></o:p></p>
<p class="MsoPlainText">* Verification of Smart Contracts<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText">SUBMISSION<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><span style="color:black">Submit original manuscripts (not published or considered elsewhere) with a page limit of 12 pages for <strong><span style="font-family:"Calibri",sans-serif;font-weight:normal">full papers</span></strong> and
6 pages for <strong><span style="font-family:"Calibri",sans-serif;font-weight:normal">short</span></strong><b> </b>and <strong><span style="font-family:"Calibri",sans-serif;font-weight:normal">tool papers<o:p></o:p></span></strong></span></p>
<p class="MsoPlainText"><span style="color:black">(excluding bibliography and short appendix of up to 5 additional pages).<o:p></o:p></span></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><span style="color:black">Alternatively you may also submit an <strong><span style="font-family:"Calibri",sans-serif;font-weight:normal">extended abstract</span></strong> of up to 3 pages (including bibliography) summarizing your ongoing
work in the area of<o:p></o:p></span></p>
<p class="MsoPlainText"><span style="color:black">formal methods and blockchain. Authors of selected extended-abstracts are invited to give a short <strong><span style="font-family:"Calibri",sans-serif;font-weight:normal">lightning talk</span></strong>. Extended
abstracts will not occur in<o:p></o:p></span></p>
<p class="MsoPlainText"><span style="color:black">the workshop proceedings.<o:p></o:p></span></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Submission link: <a href="https://easychair.org/conferences/?conf=fmbc2024">
https://easychair.org/conferences/?conf=fmbc2024</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">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="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Instructions for authors:<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><a href="https://submission.dagstuhl.de/documentation/authors#oasics">https://submission.dagstuhl.de/documentation/authors#oasics</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">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="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">PROCEEDINGS<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText"><span style="color:black">All submissions will be peer-reviewed by at least three members of the program committee for quality and relevance.<o:p></o:p></span></p>
<p class="MsoPlainText"><span style="color:black">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></span></p>
<p class="MsoPlainText"><span style="color:black">OpenAccess Series in Informatics (</span><a href="https://www.dagstuhl.de/en/publishing/series/details/oasics">OASIcs</a><span style="color:black">) by Dagstuhl.<o:p></o:p></span></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">INVITED SPEAKER<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">Franck Cassez, Head of Research, Mantle ( <a href="https://www.mantle.xyz">
https://www.mantle.xyz</a> ) <a href="https://franck44.github.io/">https://franck44.github.io/</a><o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText">PROGRAM COMMITTEE<o:p></o:p></p>
<p class="MsoPlainText">--------------------------------<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">PC CO-CHAIRS<o:p></o:p></p>
<p class="MsoPlainText">* Bruno Bernardo (Nomadic Labs, France) (<a href="mailto:bruno@nomadic-labs.com">bruno@nomadic-labs.com</a>)<o:p></o:p></p>
<p class="MsoPlainText">* 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="MsoPlainText"><o:p> </o:p></p>
<p class="MsoPlainText">PC MEMBERS<o:p></o:p></p>
<p class="MsoPlainText">* Burcu Kulahcioglu Ozkan (Delft University of Technology)<o:p></o:p></p>
<p class="MsoPlainText">* Maria Potop-Butucaru (Sorbonne University)<o:p></o:p></p>
<p class="MsoPlainText">* Bas Spitters (Aarhus University)<o:p></o:p></p>
<p class="MsoPlainText">* Sophie Rain (TU Wien)<o:p></o:p></p>
<p class="MsoPlainText">* Gordon Pace (University of Malta)<o:p></o:p></p>
<p class="MsoPlainText">* Ron Van Der Meyden (The University of New South Wales)<o:p></o:p></p>
<p class="MsoPlainText">* Maurice Herlihy (Brown University)<o:p></o:p></p>
<p class="MsoPlainText">* Vincent Rahli (University of Birmingham)<o:p></o:p></p>
<p class="MsoPlainText">* Meng Sun (Peking University)<o:p></o:p></p>
<p class="MsoPlainText">* Martin Ceresa (IMDEA Software Institute)<o:p></o:p></p>
<p class="MsoPlainText">* Massimo Bartoletti (Universita' degli Studi di Cagliari)<o:p></o:p></p>
<p class="MsoPlainText">* Denisa Diaconescu (University of Bucharest)<o:p></o:p></p>
<p class="MsoPlainText">* Manuel Chakravarty (Tweag & IOG)<o:p></o:p></p>
<p class="MsoPlainText">* Bernhard Beckert (Karlsruhe Institute of Technology)<o:p></o:p></p>
<p class="MsoPlainText">* Florian Kammueller (Middlesex University London and TU Berlin)<o:p></o:p></p>
<p class="MsoPlainText">* Baoluo Meng (GE Global Research)<o:p></o:p></p>
<p class="MsoPlainText">* Albert Rubio (Universidad Complutense de Madrid)<o:p></o:p></p>
<p class="MsoPlainText">* Sylvain Conchon (Universite Paris-Saclay)<o:p></o:p></p>
<p class="MsoPlainText">* Fritz Henglein (University of Copenhagen)<o:p></o:p></p>
<p class="MsoPlainText"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>