University of Cambridge

Job Opportunities

Jobs

PhD Studentship in Machine Learning Based Program Synthesis (Fixed Term)


Fixed-term: The funds for this post are available for 3 years from January 2020 until December 2022. Successful applicants will receive a maintenance allowance of at least the University of Cambridge's recommended maintenance per annum for 3 years and approved tuition fees at home/EU rates.

The PhD Studentship is available to work on program synthesis, which is the mechanised construction of software that provably satisfies a given specification. A traditional view of program synthesis is solver based, which makes use of theorem provers to derive a program from a given specification. Recently, machine learning techniques have started to be applied to synthesis tasks. In this project, we propose to combine solver based program synthesis with statistical program learning. The solver based architecture that we will be using is Counter-Example Guided Inductive Synthesis (CEGIS). CEGIS denotes an iterative oracle based technique where each iteration performs inductive generalisation based on counterexamples provided by a verification oracle. Current CEGIS instantiations make use of software verification techniques (e.g. bounded model checking, explicit state model checking) and, ultimately, rely on Propositional Satisfiability/Satisfiability Modulo Theories (SAT/SMT) solvers. In this project, we propose to integrate techniques from the machine learning community within a CEGIS refinement loop. In particular, we are interested in neural networks and reinforcement learning.

The position is within the Programming, Logic, and Semantics Group at the University of Cambridge's Department of Computer Science and Technology.

Candidates should have at least a first-class honour's degree in computer science or a closely related discipline. Candidates should provide evidence of relevant work, where possible, and must demonstrate a desire to perform internationally-leading research and to publish in the top programming languages and software verification conferences.

This studentship is funded by the Royal Society Research Grant for Research Fellows 2018.

For UK/EU eligible students this covers a stipend and fees.

Non-UK/EU students may require additional funding for the higher level of fees. Unless you have your own resources for meeting the additional costs of international students, you will not be eligible for this studentship. Applicants should consult the advice given on http://www.cst.cam.ac.uk/admissions/PhD about eligibility and the requirements for the research proposal.

In the Faculty of Computer Science and Technology, all first-year research students are admitted on a probationary basis, and will be registered for the Certificate of Postgraduate Studies in Computer Science. Funding in the second and subsequent years will be conditional upon successful completion of the first and second years' progress reviews and registration for the PhD Degree.

Applicants should contact Dr Cristina David (cristina.david@cl.cam.ac.uk) for further information.

Complete applications, including two academic references, research proposal, transcripts and degree certificates, should be submitted via the Applicant Portal by the 30 September 2019, see http://www.graduate.study.cam.ac.uk/how-do-i-apply.

Queries regarding the application process should be directed to clgrdadm@hermes.cam.ac.uk using the reference number below.

Please quote reference NR20458/RG98850 on your application and in any correspondence about this vacancy.

The University actively supports equality, diversity and inclusion and encourages applications from all sections of society.