Ethereum Smart Contract Analysis - SMT Solving of Complex Constraints

We have implemented a tool that analyses Ethereum Smart Contracts on scale.

Your task would be to extend that tool with a state-of-the-art SMT Solver (Z3) in order to explore feasible paths of an Ethereum Smart Contract.

For more details please make an appointment: andreas.fuchs@wi.uni-muenster.de