FindAPhD Weekly PhD Newsletter | JOIN NOW FindAPhD Weekly PhD Newsletter | JOIN NOW

Application Level Verification of Solidity Smart Contracts


   Department of Computer Science

This project is no longer listed on FindAPhD.com and may not be available.

Click here to search FindAPhD.com for PhD studentship opportunities
  Dr R Banach  Applications accepted all year round  Funded PhD Project (Students Worldwide)

About the Project

Smart contracts running in a blockchain environment (e.g. ones written in Solidity running on an Ethereum blockchain) need to consist of well defined atomic state updates; otherwise, the properties of the on-chain state become meaningless. Essentially, blockchain transactions need to enjoy the well-known ACID properties familiar from the database world. The (D)urability aspect of such transactions implies that it is practically impossible to back out of a running smart contract once it is live on the blockchain.

So, smart contracts need to be right the first time, and for this, formal verification can play a vital role. Event-B is a formalism for modelling and verifying systems whose behaviour consists of well defined atomic state updates, and is supported by the open-source Rodin toolset. This project aims to explore the feasibility of the basic Event-B framework for designing and verifying Solidity smart contracts and, will build a suitable plugin that could be added to the Rodin tool to support the design of such contracts. The project will investigate novel symbolic verification methods based on SAT modulo theories and abstract interpretation techniques in Rodin to check the discharged verification conditions.


Funding Notes

Candidates who have been offered a place for PhD study in the Department of Computer Science may be considered for funding by the Department. Further details on funding can be found at: https://www.cs.manchester.ac.uk/study/postgraduate-research/funding/.

How good is research at The University of Manchester in Computer Science and Informatics?


Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities
PhD saved successfully
View saved PhDs