Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 2.24 MB
  • 22 pages

Document Identifiers

Author Details

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
and all authors of the abstracts in this report

Cite AsGet BibTex

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". 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 in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant 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. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Software and its engineering → Formal language definitions
  • Software and its engineering → Software verification and validation
  • automated reasoning
  • cryptographic protocols
  • program verification
  • programming languages
  • smart contracts


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail