Skip to main content
KBS_Icon_questionmark link-ico

PhD Studentship: Nominal Specification and Verification Environments

Subject areas:

Computer science. Natural Sciences.

Funding type:

Stipend. Tuition fee.



3.5 year fully-funded studentship in informatics to start in either June 2025 or October 2025.

Award details

Applications are invited for a fully-funded PhD studentship to start in June 2025 or at a later date during the 2025-26 academic year. 

Project Description: 

Software verification techniques have been successfully used to prove correctness of low-level programs, but verification of high-level programming languages is challenging: it requires reasoning about name binding (e.g., visible/hidden channel names, scoping rules defining local and global variable names, parameter passing and substitution of values for variables). A standard approach to deal with name binding in verification tasks is to replace names with numerical codes (de Bruijn indices). While this avoids some of the difficulties of reasoning about names in programs, conducting a formalisation in de Bruijn style is labour-intensive and imposes a significant overhead to comprehending and reusing proofs. Nominal techniques offer an alternative, user-friendly approach, which does not require to replace names with codes.

We aim to apply novel nominal techniques to simplify the handling of names and binders in programming languages and verification tasks (e.g., verification of blockchain languages, security policies, etc). For this, we aim to develop a core nominal calculus and use it as a basis to enrich with nominal features verification frameworks such as Maude and K.

Award value

The studentships are funded for 3.5 years and include Tuition Fees, a Stipend at the UK Research Council rate (plus London weighting) and an allowance for research consumables and travel.

Eligibility criteria

Award open to UK and overseas students.

Applicants should have a First-class undergraduate degree or a Distinction at MSc level in Computer Science or Mathematics. In exceptional cases other qualifications and experience may be considered and all applications will be assessed on their merit as appropriate.

Application process

Applications should be submitted by the end of December for a start in June 2025 and by the end of May for a start in October 2025. Applications will be assessed as they arrive so submit as early as possible.

To be considered for the position candidates must apply via King’s Apply online application system. Details are available here.

To apply for this studentship funding please cite the code ‘StartUpFernandez’ in the Funding section of the application form. Please select option 5 ‘I am applying for a funding award or scholarship administered by King’s College London’ and type the code into the ‘Award Scheme Code or Name’ box. Please copy and paste the code exactly.

Applicants should email Professor Maribel Fernandez before submitting the application, and include a summary of their academic background, research interests and any relevant previous experience. 

 
 

Selection process

Applicants will be shortlisted based on the documents submitted and, if selected, will be interviewed by a panel of 2-3 academics from the Department.  

Contact Details

Professor Maribel Fernandez, Department of Informatics, Maribel.Fernandez@kcl.ac.uk

Academic year:

2024-25

Grant code:

StartUpFernandez

Study mode:

Postgraduate research

Application closing date:

31 December 2024
31 May 2025