Modeling and Verification of Smart Contracts
| Typ: | BA / MA / HiWi |
|---|---|
| Datum: | 2022-12-12 |
| Betreuer: | Jonas Schiffl |
| Aushang: |
Overview
Smart contracts are programs which run in conjunction with a blockchain or another type of distributed ledger. They function as a trusted computing platform, in the sense that anyone can be sure what transactions are made and what computations are performed, without having to run the programs themselves. Smart contracts are
-
immutable: cannot be changed after deployment
-
public: bytecode (and usually source code) is open for all to see
- attractive targets because they handle valuable assets
Therefore: Smart contracts have to be correct upon deployment!
Research Goals
Design and development of
-
a method for modeling smart contract applications in an intuitive way,
-
tools for specifying the intended behaviour,
- a process for verifying that the application works as intended and is secure against malicious agents.
How You can contribute
Are you interested in designing an abstract representation of smart contracts, and methods for verifying correctness and security properties?
Then apply for a Bachelor's or Master's thesis!
Are you interested in implementing the abstract representation and its interfaces to formal analysis tools?
Then apply as a student assistant ("Hiwi")!