https://www.dagstuhl.de/20231

01. – 05. Juni 2020, Dagstuhl-Seminar 20231

Rigorous Methods for Smart Contracts

Organisatoren

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)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Annette Beyer zu administrativen Fragen

Andreas Dolzmann zu wissenschaftlichen Fragen

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

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.