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.

Creative Commons BY 3.0 DE

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu