University College London Featured PhD Programmes
Norwich Research Park Featured PhD Programmes
Norwich Research Park Featured PhD Programmes
The Francis Crick Institute Featured PhD Programmes
University of Reading Featured PhD Programmes

Automated Verification of WebAssembly Programs

  • Full or part time
  • Application Deadline
    Applications accepted all year round
  • Self-Funded PhD Students Only
    Self-Funded PhD Students Only

Project Description

The new language WebAssembly is gaining popularity as a compilation target for Web applications. Unlike many modern languages, it has been carefully specified using a reference implementation in Standard ML. Some recent research has included production of a mechanised executable specification in Isabelle, further clarifying details of the language.

Automated verification techniques are methods for proving that a program behaves in a certain way, or is free from certain kinds of errors. Unlike testing, which only checks a finite number of use cases of a program, automated verification uses mathematically justified techniques to reason about a program, proving that it behaves correctly in all possible situations.

Automated verification techniques have developed rapidly over the last 20 years and are beginning to be used in some applications software. One common barrier to their application is the complexity and ambiguity of most programming languages. WebAssembly ought not to suffer from these problems. This factor, combined with its emerging popularity, makes it an ideal target for low-level automated verification techniques.

The goal of this project is to produce an automated verification tool for WebAssembly and to assess which verification techniques are effective for WebAssembly programs.

For informal enquiries, please contact , including "Automated Verification of WebAssembly Programs" in the subject of your e-mail and stating clearly how you meet the eligibility criteria.

Funding Notes

You must have a good Bachelor's degree (2.1 or higher, or equivalent) or Master's degree in Computer Science, Mathematics or a similar relevant subject.

Experience of software development is essential, as is some knowledge of automated verification. Advanced knowledge of automated verification is not required, but you should (for example) have studied a relevant module at postgraduate or final year undergraduate level. Knowledge of compilers is also desirable.

Related Subjects

Email Now

Insert previous message below for editing? 
You haven’t included a message. Providing a specific message means universities will take your enquiry more seriously and helps them provide the information you need.
Why not add a message here
* required field
Send a copy to me for my own records.

Your enquiry has been emailed successfully

FindAPhD. Copyright 2005-2019
All rights reserved.