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://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.exeter.ac.uk%2Fv8media%2Frecruitmentsites%2Fdocuments%2FA_Verification_Environment_for_Distributed_Systems_Implemented_in_Go_EPSRC_DLA_Project_September_2025_Entry.pdf&data=05%7C02%7Com-announce%40openmath.org%7C0a82da385f0e4a9f733f08dd450b61ce%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638742637826958968%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C40000%7C%7C%7C&sdata=%2B9pGiQdSOu%2B03P1bEPFRmX%2B52JBsA%2BkplsqtbVsk%2F30%3D&reserved=0 Information about the funding and application process is available at: * https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.exeter.ac.uk%2Fstudy%2Ffunding%2Faward%2F%3Fid%3D5477&data=05%7C02%7Com-announce%40openmath.org%7C0a82da385f0e4a9f733f08dd450b61ce%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638742637826981496%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C40000%7C%7C%7C&sdata=e%2BgQ7Y7jEqeCHhyVa%2Bobs0btjatouqHMOHH2ARup7Ko%3D&reserved=0 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://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.brucker.ch%2F&data=05%7C02%7Com-announce%40openmath.org%7C0a82da385f0e4a9f733f08dd450b61ce%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638742637826999791%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C40000%7C%7C%7C&sdata=7%2FSTAz7k%2BS7ziY2bzB0znS%2FSZCunZsV6vLr4tMfubUM%3D&reserved=0 | https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flogicalhacking.com%2Fblog&data=05%7C02%7Com-announce%40openmath.org%7C0a82da385f0e4a9f733f08dd450b61ce%7Ccc7df24760ce4a0f9d75704cf60efc64%7C0%7C0%7C638742637827014797%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C40000%7C%7C%7C&sdata=3L%2F%2F6MndjFi6GEoI2d90e9PcV0V9Ul3tGHicCErKRaM%3D&reserved=0 @adbrucker | @logicalhacking _______________________________________________ Om-announce mailing list [email protected] https://mailman.openmath.org/cgi-bin/mailman/listinfo/om-announce
