PhD Studentship – Symbolic Execution (at the intersection of programming languages, security, software engineering and systems)


Imperial College London – Department of Computing

Studentship: Untaxed bursary of £16,052 per annum (2015/16 figure including London weighting) plus home/EU/oversees fees

The Department of Computing is a leading department of Computer Science among UK Universities, and has consistently been awarded the highest research rating. In the 2014 REF assessment, The Department was ranked third (1st in the Research Intensity table published by The Times Higher), and was rated as “Excellent” in the previous national assessment of teaching quality.

Applications are invited for a PhD student in the Software Reliability Group of the Department of Computing at Imperial College London, under the direction of Dr Cristian Cadar. Symbolic execution is a program analysis technique that has gained tremendous popularity in the last decade, becoming part of the standard toolbox of techniques in many computer science fields including software engineering, programming languages, software testing, verification, security, and computer systems. The technique has enabled a wide range of applications, including the automatic detection of bugs and security vulnerabilities, recovery of corrupt documents, patch generation, and automatic debugging, among many others.

Despite its strengths, symbolic execution faces important scalability and deployment challenges that have prevented wide adoption in practice. The goal of this project is to make significant progress towards industrial adoption by designing and implementing innovative solutions addressing these challenges, including those related to the analysis of binary code and the way an application interacts with its environment. These techniques will be investigated in the context of KLEE, a modern symbolic execution system maintained in our research group. For more information on KLEE and symbolic execution in general, we recommend reading the paper at https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf.

To apply for this position, you will need to have a strong background in at least one of the following areas: compilers/program analysis, programming languages or operating systems. You will also need experience in building and working with large software systems and tools. Prior experience with LLVM, KLEE and binary analysis tools is a plus, but not required.

Applicants should have a Master’s degree in Computer Science or a related field, and good communication and technical writing skills.

The position is fully funded, covering tuition fees, travel funds and a stipend/bursary. The position is available to both EU and overseas students.

How to apply

To apply for this position, please follow the instructions at http://www.imperial.ac.uk/computing/prospective-students/courses/phd/.

In the application form, please write ‘Symbolic execution’ in the ‘Proposed Research Topic’ field, and ‘Cristian Cadar’ in the ‘Proposed Research Supervisor field.

Early applications are encouraged. Informal inquiries about this position are also encouraged and can be directed to Dr Cristian Cadar [email protected] . For further information on the group and related projects see the group website at https://srg.doc.ic.ac.uk/.

This position will be based at the South Kensington campus in central

Applicants are advised to visit http://www3.imperial.ac.uk/computing/research/degrees for general information on becoming a PhD student in the Department of Computing


Leave a Reply