Specification and Functional Verification of Smart Contracts

Software Campus

Smart contracts are programs that are executed in a blockchain, mapping contracts and other real-world agreements to program logic and executing the contract conditions in an automated and transparent manner. Typical use cases range from business relationships, with the blockchain acting as a secure database and fraud protection, to voting, where security and privacy can be guaranteed by blockchain technology.

Smart contracts require a high degree of reliability. They manage financial goods, rights, and other real-world values, making them a potential target for attackers. Therefore it is necessary to use formal methods when designing smart contracts, so that their functional correctness can be proven.

The goal of this project is to pave the way for specification and formal verification of smart contracts. Building on existing verification tools and technology, we establish a base for describing and proving functional properties of smart contracts. The overall goal is that blockchain/smart-contract technology, with all its advantages, can be confidently employed.

The project is led by Prof. Bernhard Beckert and managed by Jonas Schiffl. It is part of the BMBF-funded Software Campus project. We cooperate with partners from DATEV eG.


Name Role Phone Email
Leader +49 721 608-44025 beckert1677716050Xfd4∂
Manager +49 721 608-45252 jonas.schiffl1585323865Xfd4∂
Member +49 721 608-43856 herda573968443Xfd4∂
Michael Kirsten Member +49 721 608-45648 kirsten1174711121Xfd4∂