Skip to main content

Funding and scholarships for students

Award details

Compositional Verification of Smart Contracts in Isabelle. EMPS College Home fees Studentship, PhD in Computer Science. Ref: 4326

About the award

Supervisors

Lead Supervisor:

Dr. Diego Marmsoler, College of Engineering, Mathematics and Physical Sciences, Streatham Campus, University of Exeter

Co-supervisor: 

Prof. Achim D. Brucker, College of Engineering, Mathematics and Physical Sciences, Streatham Campus, University of Exeter

Location:

Department of Computer Science, Streatham Campus, Devon, University of Exeter

The University of Exeter’s College of Engineering, Mathematics and Physical Sciences  is inviting applications for a fully-funded PhD studentship to commence in January 2022 or as soon as possible thereafter. The studentship will cover Home tuition fees plus an annual tax-free stipend of at least £15,609 for 3.5 years full-time, or pro rata for part-time study. 

This College studentship is open to UK and Irish nationals, who if successful in their application will receive a full studentship including payment of university tuition fees at the home fees rate.

Project Description:

With the emergence of cryptocurrencies, blockchain technologies have become more and more important. Since then, the technology found applications in several domains, such as financial, healthcare, land management, business process management, or even identity management. Smart contract is code which is deployed to a blockchain and which can be executed by sending special transactions to it. As of now, smart contracts are mainly used to automatize financial transactions. However, they have also potential to be used for other domains, such as healthcare.

Since smart contracts are deployed to the blockchain they are visible to everyone and subject to attacks. In June 17 in 2016, for example, a vulnerability in an Ethereum smart contract was exploited resulting in a loss of approximately 3:5 billions of Ether (at that time corresponding to roughly $50 billion). In the healthcare sector, the impact of bugs in smart contracts may be even worse since it may threaten the live of patients.

To address this problem, attempts have been made to support the verification of smart contracts developed in a programming language, such as Solidity. To this end, a security property can be specified for the smart contract and the implementation of the contract in Solidity is then verified against the property. If the verification is successful, the smart contract is guaranteed to satisfy the original property.

Most of the work so far focuses on the verification of single smart contracts. However, modern smart contract applications consist of several smart contracts which often depend on one another. The aim of this project is to investigate how to verify such applications using an interactive theorem prover such as Isabelle and in particular how to apply compositional techniques to minimize the verification effort.

For the purpose of this project, we are looking for enthusiastic and outstanding Computer Science or Mathematics students with a strong background in some of the following topics:
• formal modelling or formal reasoning/verification,
• program analysis or program verification,
• semantics of programming languages,
• theorem proving,
• distributed systems and blockchain

Entry requirements

This studentship is open to UK and Irish nationals, who if successful in their application will receive a full studentship including payment of university tuition fees at the home fees rate.

Applicants for this studentship must have obtained, or be about to obtain, a First or Upper Second Class UK Honours degree, or the equivalent qualifications gained outside the UK, in an appropriate area of science or technology. 

If English is not your first language you will need to have achieved at least 6.0 in IELTS and no less than 6.0 in any section by the start of the project. 

Alternative tests may be acceptable (see http://www.exeter.ac.uk/postgraduate/apply/english/).

How to apply

In the application process you will be asked to upload several documents.  Please note our preferred format is PDF, each file named with your surname and the name of the document, eg. “Smith – CV.pdf”, “Smith – Cover Letter.pdf”, “Smith – Transcript.pdf”.

• CV
• Letter of application (outlining your academic interests, prior project work experience and reasons for
  wishing to undertake the project).
• Transcript(s) giving full details of subjects studied and grades/marks obtained (this should be an
   interim transcript if you are still studying)
• Two references from referees familiar with your academic work. If your referees prefer, they can email
   the reference direct to pgrenquiries@exeter.ac.uk quoting the studentship reference number.
• If you are not a national of a majority English-speaking country you will need to submit evidence of your proficiency in English.  Please see the entry requirements information above.

The closing date for applications is midnight on 24th January 2022.  Interviews will be held online on the week commencing 7th February 2022.

If you have any general enquiries about the application process please email pgrenquiries@exeter.ac.uk

Project-specific queries should be directed to the main supervisor at d.marmsoler@exeter.ac.uk

Summary

Application deadline:24th January 2022
Value:Home tuition fees plus an annual tax-free stipend of at least £15,609 for 3.5 years full-time, or pro rata for part-time study.
Duration of award:per year
Contact: PGR Admissions Office pgrenquiries@exeter.ac.uk