EPSRC Doctoral Landscape Award: The University of Exeter invites applications for a fully funded PhD position under the Engineering and Physical Sciences Research Council (EPSRC) Doctoral Landscape Award. This project aims to develop a formal verification environment for Go (Golang), a widely used programming language for security-critical distributed systems. The research will contribute to enhancing safety, security, and privacy in critical infrastructures, ensuring compliance with emerging software liability laws.
Title: A Verification Environment for Distributed Systems Implemented in Go
Designation: PhD Candidate
Research Area: Formal Methods, Security, Distributed Systems, Software Verification
Location: Innovation Centre, Streatham Campus, University of Exeter, UK
Eligibility/Qualification:
- Candidates must have an undergraduate or master’s degree in Computer Science, Software Engineering, Mathematics, Cyber Security, or a closely related field.
- Strong background in formal methods (program reasoning, programming language semantics, model checking, theorem proving, computational logic).
- Familiarity with distributed systems, communication protocols, and the Go (Golang) programming language is desirable.
Job Description:
- Develop a novel verification framework for Go within an interactive theorem prover (e.g., Isabelle/HOL).
- Define a formal semantics of Go in Higher-Order Logic (HOL).
- Build verification tools, such as a verification condition generator.
- Focus on security- and safety-critical distributed systems.
- Validate the framework using a real-world case study provided by an industrial partner specializing in secure, distributed data storage.
- Work under the guidance of leading experts Prof. Achim D. Brucker (Exeter), Dr. Diego Marmsoler (Exeter), and Prof. Burkhart Wolff (University Paris-Saclay, France).
How to Apply:
Interested candidates should contact Prof. Dr. Achim Brucker (a.brucker@exeter.ac.uk) to discuss their application.
Applicants must ensure they meet the entry requirements of the PhD in Computer Science programme. To apply, please visit the official application portal click here.
Last Date to Apply:
Applications are open until filled, but early submission is encouraged.
Project Partner: University Paris-Saclay, France
Keywords: security, safety, formal verification, program semantics, Go, Golang, distributed systems
This PhD project offers an exciting opportunity to contribute to cutting-edge research in software verification while working with renowned academics and industry partners. Apply now to be part of this transformative initiative!
