[Haskell] PhD Position: Verification of Golang using Interactive Theorem Proving (Application Deadline 2025-02-10)

[Achim D. Brucker]

We have an exciting funded opportunity for a PhD on developing "Verification Environment for Distributed Systems Implemented in Go". The main objectives are to define a formal semantics of Go and its CSP-inspired concurrency model in an interactive theorem prover (e.g., Isabelle/HOL) as well as developing a calculus for program verification. This is a unique opportunity to work in the intersection of theory and application and while doing so, contributing to improving the state of the art in software correctness and security. 

A detailed description of the PhD proposal is available at:

* https://www.exeter.ac.uk/v8media/recruitmentsites/documents/A_Verification_Environment_for_Distributed_Systems_Implemented_in_Go_EPSRC_DLA_Project_September_2025_Entry.pdf

Information about the funding and application process is available at:

* https://www.exeter.ac.uk/study/funding/award/?id=5477

Application deadline is the midnight GMT on 10th of February 2025.

Please reach out to me, if you have any questions. 

Best,
	Achim 

-- 
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter
           https://www.brucker.ch | https://logicalhacking.com/blog
                         @adbrucker | @logicalhacking