October 24 – 29 , 2021, Dagstuhl Seminar 21431

Rigorous Methods for Smart Contracts


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)

For support, please contact

Dagstuhl Service Team


Aims & Scope
List of Participants
Dagstuhl Seminar Schedule [pdf]


The seminar attracted 22 on-site and approximately as many off-site participants. The hybrid mode presented an opportunity for collaborators, particularly students, of invitees to participate remotely and contribute to the discussions. Remote participation spanned all time zones which attested to their involvement. The on-site participants had the benefit of extended interactions and relation building so crucial for advancing scientific activities.

The technical program was organized around first day of tutorial presentations on the main topics covered by the seminar. These topics were static analysis techniques, program verification methods, protocol design for decentralized ledgers, and semantic-based tools.

The following days provided for in-depth sessions around these topics. Static analysis techniques spanned using Horn clause solvers, Datalog engines, and abstract interpretation frameworks in a mixture of academic and industrial settings. Program verification techniques, likewise, were pursued both by academic and industry participants. The seminar offered an excellent forum for the scientific and commercial community around smart contracts to exchange experiences and develop ideas.

For the social program, we hiked for two hours during a beautiful October afternoon to Landgasthof Paulus & Der Laden for a delightful dinner.

Summary text license
  Creative Commons BY 4.0
  Nikolaj S. Bjørner


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


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


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).

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.


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