<div dir="ltr"><div>6th International Workshop on Formal Methods for Blockchains - First Call for Papers</div><br><a href="https://urldefense.com/v3/__https://fmbc.gitlab.io/2025__;!!IBzWLUs!WPAhtzeYTE9-MRw7-1txh1v8LJmceJOJ73awEi43SngdPfdT9_nfXxwtqDTmCtSfmE8GRbX2XOOMN3nOcb7yB6LTmPYL$" target="_blank">https://fmbc.gitlab.io/2025</a><br><br>May 04, 2025, Hamilton, ON, Canada<br><br>Co-located with the European joint conferences on theory and practice of software (ETAPS 2025)<br><br><a href="https://urldefense.com/v3/__https://www.etaps.org/2025/__;!!IBzWLUs!WPAhtzeYTE9-MRw7-1txh1v8LJmceJOJ73awEi43SngdPfdT9_nfXxwtqDTmCtSfmE8GRbX2XOOMN3nOcb7yBzoyKrMo$" target="_blank">https://www.etaps.org/2025/</a><div><br></div><div>--------------------------------------------------------------------------<br>--------------------------------------------------------------------------<br>TOPICS OF INTEREST<br>--------------------------------------------------------------------------<br><br>Blockchain is a novel technology to store data in a decentralized way.<br>Although the technology was originally invented to enable cryptocurrencies, it quickly found applications in several other domains.<br><br>Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are<br>stored in the blockchain and that run on the network. They can interact with the ledger’s data and update its state.<br>These scripts can express the logic of possibly complex contracts between users of the blockchain. Thus, Smart Contracts can facilitate<br>the economic activity of blockchain participants.<br><br>Since blockchains are often used to store financial transactions, bugs may result in huge economic losses and thus it is now of utmost<br>importance to have strong guarantees of the behaviour of blockchain software. These guarantees can be brought by using Formal Methods.<br>Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools is relevant:<br>consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to<br>write smart contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc.<br><br>This workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology.<br>Topics include, but are not limited to:<br>* Formal models of Blockchain applications or concepts<br>* Formal methods for consensus protocols<br>* Formal methods for Blockchain-specific cryptographic primitives or protocols<br>* Design and implementation of Smart Contract languages<br>* Verification of Smart Contracts<br>* Zero-knowledge proof and its applications in a blockchain setting</div><div><br></div><div><br></div><div>--------------------------------------------------------------------------<br>--------------------------------------------------------------------------<br>SUBMISSION<br>--------------------------------------------------------------------------<br><br>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<br>(excluding bibliography and short appendix of up to 5 additional pages).<br><br>Alternatively you may also submit an extended abstract of up to 3 pages (including bibliography) summarizing your ongoing work in the area of<br>formal methods and blockchain. Authors of selected extended-abstracts are invited to give a short lightning talk. Extended abstracts will not occur in<br>the workshop proceedings.<br><br>Submission link: <a href="https://urldefense.com/v3/__https://easychair.org/conferences/?conf=fmbc2025__;!!IBzWLUs!WPAhtzeYTE9-MRw7-1txh1v8LJmceJOJ73awEi43SngdPfdT9_nfXxwtqDTmCtSfmE8GRbX2XOOMN3nOcb7yBxL3xs1n$" target="_blank">https://easychair.org/conferences/?conf=fmbc2025</a><br><br>Authors are encouraged to use LaTeX and prepare their submissions according to the instructions and styling guides for OASIcs provided by Dagstuhl.<br><br>Instructions for authors:<br><br><a href="https://urldefense.com/v3/__https://submission.dagstuhl.de/documentation/authors*oasics__;Iw!!IBzWLUs!WPAhtzeYTE9-MRw7-1txh1v8LJmceJOJ73awEi43SngdPfdT9_nfXxwtqDTmCtSfmE8GRbX2XOOMN3nOcb7yByXRfW4X$" target="_blank">https://submission.dagstuhl.de/documentation/authors#oasics</a><br><br>At least one author of an accepted paper is expected to present the paper at the workshop as a registered participant.</div><div><br></div><div>--------------------------------<br>--------------------------------<br>PROCEEDINGS<br>--------------------------------<br><br>All submissions will be peer-reviewed by at least three members of the program committee for quality and relevance.<br>Accepted regular papers (full, short, and tool papers) will be included in the workshop proceeding, which will be published as a volume of the<br>OpenAccess Series in Informatics (OASIcs) by Dagstuhl.</div><div><br></div><div><br></div><div>--------------------------------<br>--------------------------------<br>PROGRAM COMMITTEE<br>--------------------------------<br><br>PC CO-CHAIRS<br>* Diego Marmsoler (University of Exeter, UK) (<a href="mailto:D.Marmsoler@exeter.ac.uk" target="_blank">D.Marmsoler@exeter.ac.uk</a>)<br>* Meng Xu (University of Waterloo, Canada) (<a href="mailto:meng.xu.cs@uwaterloo.ca" target="_blank">meng.xu.cs@uwaterloo.ca</a>)<br><br>PC MEMBERS<br>* Massimo Bartoletti (University of Cagliari)<br>* Bernhard Beckert (Karlsruhe Institute of Technology)<br>* Franck Cassez (Movement Labs)<br>* Denisa Diaconescu (University of Bucharest)<br>* Maurice Herlihy (Brown University)<br>* Sebastian Holler (Max Planck Institute for Security and Privacy)<br>* Enrico Lipparini (University of Genoa)<br>* Fan Long (University of Toronto)<br>* Orestis Melkonian (Input Output (IOG))<br>* Baoluo Meng (GE Aerospace Research)<br>* Burcu Kulahcioglu Ozkan (Delft University of Technology)<br>* Gordon Pace (University of Malta)<br>* Vincent Rahli (University of Birmingham)<br>* Sophie Rain (TU Wien)<br>* Augusto Sampaio (Federal university of Pernambuco)<br>* Derek Sorensen (Certora)<br>* Bas Spitters (Aarhus University)<br>* Meng Sun (Peking University)<br>* Mark Utting (The University of Queensland)<br>* Adele Veschetti (TU Darmstadt)<br>* Christoph Weidenbach (Max Planck Institute for Informatics)<br>* Teng Zhang (Aptos Labs)</div></div>