The Automation Group, within the Department of Electrical Engineering conducts research on formal verification of safety and security of smart contracts. Smart contracts are computer programs that change the way future business and trade are executed. The smart contracts are openly stored and executed in a blockchain ecosystem, enforcing a contractual agreement between mutually distrusting users, including the exchange of crypto currencies. An important feature of smart contracts is that once they are deployed on the blockchain they cannot be changed. Smart contracts successfully address the problem of guaranteeing the execution of agreements in a setting where parties neither need to trust each other, nor do they need to involve a third party (like bank, layer, or authority). At the same time, they provide a surface for security attacks.
Given the high usage of smart contracts in a variety of applications such as insurance, supply chain, etc., and the large volume of digital assets being transferred, there is strong demand for verification techniques. Formal verification is the process of mathematically proving or disproving that a model of the system satisfies some requirements. The automation group has a solid track record and solid research on formal verification of manufacturing systems and software verification of autonomous vehicles, and production systems. These approaches we now want to develop for and apply to the verification of smart contracts
Information about the division
The Automation group has a wide span, from theoretical foundations to applied systems development. We provide high-quality education at Bachelor’s, master and graduate levels. We also have extensive national and international collaborations with academia and industry.