https://www.dagstuhl.de/20231

June 1 – 5 , 2020, Dagstuhl Seminar 20231

Rigorous Methods for Smart Contracts

Organizers

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

For support, please contact

Annette Beyer for administrative matters

Andreas Dolzmann for scientific matters

Motivation

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.

Motivation text license
  Creative Commons BY 3.0 DE
  Nikolaj S. Bjorner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Classification

  • Security / Cryptology
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

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

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.