Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 20231

Rigorous Methods for Smart Contracts Postponed

( Jun 01 – Jun 05, 2020 )

Please use the following short url to reference this page:

Dagstuhl Seminar 21431: Rigorous Methods for Smart Contracts (2021-10-24 - 2021-10-29) (Details)




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:

  1. 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.
  2. 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.
  3. Connect automated-reasoning experts with domains of relevance for smart contracts.
Copyright Nikolaj S. Bjorner, Maria Christakis, Matteo Maffei, and Grigore Rosu

  • Nikolaj S. Bjørner (Microsoft Research - Redmond, US) [dblp]
  • Maria Christakis (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Matteo Maffei (TU Wien, AT) [dblp]
  • Grigore Rosu (University of Illinois - Urbana-Champaign, US) [dblp]

  • security / cryptology
  • semantics / formal methods
  • verification / logic

  • Smart Contracts
  • Program Verification
  • Programming Languages
  • Cryptographic Protocols
  • Automated Reasoning