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

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.

The Department of Computing at Imperial College London is a leading department of computer science, with a strong international presence in areas relevant to this position, such as programming languages and software engineering.

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

Description and requirements

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 this paper.

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 this link. 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. For further information on the group and related projects see the group website.