Dagstuhl Seminar 21431
Rigorous Methods for Smart Contracts
( Oct 24 – Oct 29, 2021 )
- Nikolaj S. Bjørner (Microsoft - Redmond, US)
- Maria Christakis (MPI-SWS - Kaiserslautern, DE)
- Matteo Maffei (TU Wien, AT)
- Grigore Rosu (University of Illinois - Urbana-Champaign, US)
- Andreas Dolzmann (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover : article in International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2022 - Dill, David; Grieskamp, Wolfgang; Park, Junkil; Xu, Meng; Zhong, Emma; Qadeer, Shaz - Berlin : Springer, 2022. - pp. 183-200 - (Lecture notes in computer science ; 13243 : article).
Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management.
Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research on smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is active development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Rigorous methods share a common reliance on automated-reasoning to enable smart-contract scenarios that suggest new automated-reasoning challenges.
This Dagstuhl Seminar aims to bring together leading researchers and practitioners in the areas of Program Analysis and Verification, Programming Languages, Cryptography as well as Automated Reasoning. The overarching goal of the seminar is creating a forum for advancing state-of-the-art methods for reliable smart-contract technologies.
We will anchor the seminar around a handful of tutorials and focus the presentation and discussion around the following main topics:
- Language Technologies for Reliable Contracts
- Verification Techniques for Smart Contracts
- Trusted Virtual Machines
- Reliable Distributed Computation
The objectives of the seminar are to:
- Provide practitioners of blockchain technologies access to researchers developing main advances in programming-language, verification, and cryptographic techniques, paving the way toward reliable infrastructures for smart contracts.
- Infuse the verification and programming-language communities with new insights on practical developments in blockchain deployments, cryptographic foundations for smart contracts, and advances in automated reasoning. This will enable programming-language and verification experts to develop approaches that are most suitable for current practical trends and best grounded in available technologies.
- Connect automated-reasoning experts with domains of relevance for smart contracts.
The seminar attracted 22 on-site and approximately as many off-site participants. The hybrid mode presented an opportunity for collaborators, particularly students, of invitees to participate remotely and contribute to the discussions. Remote participation spanned all time zones which attested to their involvement. The on-site participants had the benefit of extended interactions and relation building so crucial for advancing scientific activities.
The technical program was organized around first day of tutorial presentations on the main topics covered by the seminar. These topics were static analysis techniques, program verification methods, protocol design for decentralized ledgers, and semantic-based tools.
The following days provided for in-depth sessions around these topics. Static analysis techniques spanned using Horn clause solvers, Datalog engines, and abstract interpretation frameworks in a mixture of academic and industrial settings. Program verification techniques, likewise, were pursued both by academic and industry participants. The seminar offered an excellent forum for the scientific and commercial community around smart contracts to exchange experiences and develop ideas.
For the social program, we hiked for two hours during a beautiful October afternoon to Landgasthof Paulus & Der Laden for a delightful dinner.
- Elvira Albert (Complutense University of Madrid, ES) [dblp]
- Leonardo Alt (Ethereum - Berlin, DE) [dblp]
- Nikolaj S. Bjørner (Microsoft - Redmond, US) [dblp]
- Maria Christakis (MPI-SWS - Kaiserslautern, DE) [dblp]
- Marco Eilers (ETH Zürich, CH) [dblp]
- Grzegorz Fabianski (University of Warsaw, PL) [dblp]
- Josselin Feist (Trail of Bits Inc. - New York, US) [dblp]
- Bryan Ford (EPFL Lausanne, CH) [dblp]
- Diego Garbervetsky (University of Buenos Aires, AR) [dblp]
- Isabel Garcia-Contreras (IMDEA Software - Madrid, ES) [dblp]
- Arthur Gervais (Imperial College London, GB) [dblp]
- Neville Grech (University of Malta - Msida, MT) [dblp]
- Wolfgang Grieskamp (Facebook - Bellevue, US) [dblp]
- Fritz Henglein (University of Copenhagen, DK) [dblp]
- Matteo Maffei (TU Wien, AT) [dblp]
- Alexander Nutz (Certora - Berlin, DE) [dblp]
- Sophie Rain (TU Wien, AT) [dblp]
- Albert Rubio (Complutense University of Madrid, ES) [dblp]
- Tanja Schindler (Universität Freiburg, DE) [dblp]
- Yannis Smaragdakis (University of Athens, GR) [dblp]
- Valentin Wüstholz (ConsenSys - Kaiserslautern, DE) [dblp]
- Massimo Bartoletti (University of Cagliari, IT) [dblp]
- Andreea Buterchi (MPI-SWS - Kaiserslautern, DE)
- Jing Chen (Stony Brook University, US) [dblp]
- Shuo Chen (Microsoft Research Asia - Beijing, CN) [dblp]
- Ankush Das (Amazon - Cupertino, US) [dblp]
- Stefan Dziembowski (University of Warsaw, PL) [dblp]
- Ákos Hajdu (Budapest Univ. of Technology & Economics, HU) [dblp]
- Aniket Kate (Purdue University - West Lafayette, US) [dblp]
- Markulf Kohlweiss (University of Edinburgh, GB) [dblp]
- Igor Konnov (Informal Systems - Wien, AT) [dblp]
- Yi Li (Nanyang TU - Singapore, SG) [dblp]
- Victor Luchangco (Algorand - Boston, US) [dblp]
- Anastasia Mavridou (NASA - Moffett Field, US) [dblp]
- Noam Rinetzky (Tel Aviv University, IL) [dblp]
- Grigore Rosu (University of Illinois - Urbana-Champaign, US) [dblp]
- Giulia Scaffino (TU Wien, AT)
- Gerardo Schneider (University of Gothenburg, SE) [dblp]
- Ilya Sergey (National University of Singapore, SG) [dblp]
- Zhong Shao (Yale University - New Haven, US) [dblp]
- Philip Wadler (University of Edinburgh, GB) [dblp]
- Yoni Zohar (Bar-Ilan University - Ramat Gan, IL)
- security / cryptology
- semantics / formal methods
- verification / logic
- Smart Contracts
- Program Verification
- Programming Languages
- Cryptographic Protocols
- Automated Reasoning