Departmental Research Internships

Departmental Research Internships offer intermediate-year (i.e. not first or final) students in the Department of Computer Science the opportunity to gain research experience with one of the department’s world-leading research groups.  The internships take place during the summer vacation.

Students will undertake a project under the supervision of one or more members of staff in the department.  The project lasts for between eight and ten weeks and can take place between the end of the exam period and the start of the new academic year (by arrangement between student and supervisor).  Students will be provided with necessary software and equipment to undertake the work.

Interns will be employed and paid in accordance with UCL Internship Policy (, accrue annual leave, and be entitled to statutory sick pay and other pay (see the policy for further details).  Currently the rate of pay is £10.20 per hour (the London Living Wage)with the expectation of no more than a 36.5 hr working week during the summer vacation.  Interns are subject to UKVI Right to Work in the UK requirements.

The department plans to fund up to 5 internships this year.

Summer Research Internships 2018

1. A Chatbot Toolkit for Interfacing Decision Support Systems

Supervisor: Prof. Anthony Hunter

The project is on developing a chatbot toolkit for interfacing decision support systems. Each chatbot that is built using the toolkit is intended to work in a narrow domain. Furthermore, there is a high expectation that each statement input by the user is the same or similar to statements that the chatbot already knows. So a key research challenge is for the chatbot to determine which statement the input corresponds to. Techniques from computational linguistics will be used to address this challenge. So overall the project will involve implementing the modules for the toolkit, and addressing the research challenge.


2. Bringing Separation Logic to Integrated Development Environments

Supervisor: Dr Ilya Sergey

Facebook Infer is a tool for fast and precise modular analysis of large software projects implemented in C and Java. Developed initially by a group of researchers from UCL, Queen Mary and Imperial College

London, Infer is now made publicly available and is used by hundreds of developers world-wide. The heart of Infer is Separation Logic---a logical framework for specifying and verifying imperative heap-manipulating programs in a natural and scalable way.

Despite its success in finding bugs in large software code bases (such as Android SDK), Infer is still considered a standalone tool outside a standard toolbox of a working Java programmer. The goal of this project is to bring Infer to modern Integrated Development Environments (IDEs) and implement a support for Infer-based static code analysis on top of IntelliJ IDEA. The project will combine the engineering effort (i.e., learning and using the IntelliJ plugin API for implementing Infer support) with a number of research tasks required for adapting Separation Logic-based specifications for the gradual analysis of constantly changing Java code.


Good programming skills in Java/Scala/Kotlin, desire to learn about program analysis and verification

Preliminary reading and resources:

- Facebook Infer (

- IntelliJ IDEA (

- A Primer on Separation Logic (

- Moving Fast with Software Verification (


3. Towards a Verified Compiler for Smart Contracts

Supervisor: Dr Ilya Sergey

Smart contracts are a mechanism to associate executable code with certain blockchain transactions, providing a machinery for trusted decentralised arbitration, which gained a lot of attention thanks to its highly influential implementation in Ethereum. Because of the nature of the blockchain protocol, the executable code of a smart contract, once deployed, is replicated across multiple nodes participating in a consensus and cannot be changed or withdrawn. In this setting, the challenge of having correct contracts becomes particularly acute, and several research proposals have been made recently towards better programming language abstractions and verification approaches for formal mechanised reasoning about smart contracts.

This project will tackle a problem of implementing a certified compiler from a model stateful language for smart contracts to a series of existing contract back-ends, such as EVM and Michelson. We will use state-of-the art tools for certified programming and interactive theorem proving, such as Coq and Isabelle, and will adopt the ideas of existing successful efforts in verified compilers, such as CompCert and CakeML.





4. Decomposing Distributed Protocols

Supervisor: Dr Ilya Sergey

Distributed systems are ubiquitous in many aspects of modern life, such as health care, online commerce, transportation, entertainment and cloud-based applications. Given the importance of distributed software and its complexity, it is nowadays considered vital to have a rigorous verification methodology for establishing its correctness properties, ensuring that, once a distributed system is up and running, it will never go wrong and will eventually complete its goals.

In this project, we will explore the use of interactive proof assistants as a way to establish correctness properties for distributed protocols. The goal of this research internship is to implement a library of reusable verified distributed components, such as failure detection, recovery and state replication, enabling construction of scalable, robust and correct distributed protocols.


Understanding of basic principles of distributed computing, functional programming and logic.

Preliminary reading:


5. Learning appearance, illumination and shading models for surgical scenes

 Supervisor: Dr Dan Stoyanov

The project is on using machine learning (deep learning) in order to train models that estimate the appearance of objects. The focus is on surgical objects (organs and instruments) which are typically exposed to strong halogen illumination and exhibit interesting reflectance properties because they are wet. Hand modelling this reflectance behaviour is difficult and often not realistic. There is an interesting opportunity to avoid this by using CNNs/GANs and other architectures of neural networks which are the current method of choise for many problems in computer vision. Because we have robots and surgical cameras data is abundant for training such systems. Effects such as smoke can also be present in the scene to add further complexity if this is of interest to the candidate.

 Good to haves:

- Good analytical skills and some experience with programming with python/matlab

- Familiarity with a deep learning toolkits

- Good communication, work ethic and team skills

Application Process for Students

Students wishing to apply for a research bursary should consult the list of project proposals from members of staff above. If a project is of interest, please contact the member of staff concerned  to arrange an initial discussion.

Each supervisor will run a "fair and open" ( procedure to select one or more students for their internship(s). Once a student and supervisor have agreed on a project, the supervisor will take over the application process.

Deadline for contacting staff is 14 March 2018.

Application Process for Supervisors

Supervisors wishing to propose projects should email these to Ilya Sergey as soon as possible. 

Once a student has expressed interest in a project, please arrange a meeting to discuss the timing, detail and so forth.  If more than one student is interested, please arrange a fair process of assessing who is the most appropriate to take forward (e.g. a simple standard interview).

If you are happy that the student is suitable and you can agree appropriate dates, please apply for funding. The application should take the form of a one-page A4 case for support.  This should:

  • Outline the project, giving a justification for the work being undertaken by the student and how it will help to give them research experience.
  • Provide a summary of how the student will benefit from the project with regard to their career objectives.
  • Contain a summary of the student's academic performance in previous years.
  • Outline arrangements for supervision.
  • Specify the amount of subsistence expenses funding requested in weeks, plus the costs of any necessary software licences or other equipment that may be required.

The case should be emailed to Ilya Sergey by 21 March 2018.  Decisions will be made shortly thereafter.  Late applications will be accepted but may not receive funding if it has already been allocated.

Successful applicants should subsequently liaise with Dawn Bailey and JJ Giwa to arrange for their student’s financial and space provisions, and put themselves in a position to deliver the necessary induction to the student on the first day (health and safety briefing etc).

Only a single internship application on behalf of a student should be made. This requires each supervisor to choose the most suitable student for that project. This also means that each student needs to decide which is the most suitable project (in agreement with the supervisor).

Funding decisions are made on the basis of the student’s past exam performance and the project’s value to the student. The highest ranked applications will be supported, subject to the availability of funds.  Supervisors will be notified shortly after the closing date for applications.

Research Group Bursaries

For projects wholly funded by the research group associated to the project, the student should contact the named researcher directly. In these cases, the research group should still make arrangements with Dawn Bailey and JJ Giwa for finance and space, informing Chris Clack, and taking note of UCL Internship Policy regarding the recruitment and management of interns.

Information regarding visiting students

Staff can find details of this on the Intranet here.