VeriSmart
Specification and Functional Verification of Smart Contracts
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.
People
| Name | Role | Phone | |
|---|---|---|---|
| Bernhard Beckert | Leader | +49 721 608-44025 | beckert319374814Xfd4∂kit.edu |
| Jonas Schiffl | Manager | +49 721 608-45252 | jonas.schiffl1063654055Xfd4∂kit.edu |
| Mihai Herda | Member | +49 721 608-43856 | herda1007412186Xfd4∂kit.edu |
| Michael Kirsten | Member | +49 721 608-45648 | kirsten1839686771Xfd4∂kit.edu |
