DROPS

Document

Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)

Authors: Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, and Wietze Koops

Published in: Dagstuhl Reports, Volume 15, Issue 6 (2026)

Abstract

Modern automated reasoning has transformed large parts of industry and has also found numerous scientific applications. But many reasoning problems are computationally very challenging, or sometimes even undecidable. Because of this, the reasoning algorithms used are often very complex, and even the best current algorithms at times produce wrong results. As these tools are increasingly being used autonomously, sometimes even in life-critical applications, it is urgent to ensure that what they compute is valid. Software testing, while immensely useful, cannot guarantee correctness, and state-of-the-art algorithms are far beyond what techniques for producing formally verified software can handle. The focus of this Dagstuhl Seminar was the approach of addressing such issues by designing certifying algorithms using so-called proof logging, meaning that algorithms output not only a result but also a machine-verifiable proof of correctness. This proof can then be fed to a dedicated proof checker for verification. Crucially, such proofs should require low overhead to generate and be easy to check, but still supply 100% correctness guarantees. Besides ensuring correctness of outputs for complex algorithms, proof logging can also provide new tools for algorithm development and analysis, software debugging, and even research into explainability in the context of AI.

Cite as

Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, and Wietze Koops. Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231). In Dagstuhl Reports, Volume 15, Issue 6, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.15.6.1,
  author =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  title =	{{Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)}},
  pages =	{1--31},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{6},
  editor =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.1},
  URN =		{urn:nbn:de:0030-drops-255798},
  doi =		{10.4230/DagRep.15.6.1},
  annote =	{Keywords: ATP, Computer Algebra, DRAT, DRUP, MIP, Propagation Redundancy, QBF, SAT, SMT}
}

Document

DOI: 10.4230/DagRep.11.9.80

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

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

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)

Abstract

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.

Cite as

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)

Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}

Search Results

Documents authored by Bjørner, Nikolaj S.

Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)

Abstract

Cite as

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Abstract

Cite as

Thanks for your feedback!

Could not send message