<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">We in Swansea are advertising a job position which would be suitable for experts in Agda, Coq, or related systems, or type theoretists in general. We have a cyber security group, and a very active railway verification group, here in Swansea.
I have done some work on verification of Bitcoin and Solidity in Agda, and with my former PhD student Karim Kanso I have carried out some substantial research on verifying railway interlocking systems in Agda.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">In the area of railway verification we have a well established long term collaboration with Siemens Mobility. It would be nice to get somebody who uses Agda or some other type theoretic approach, or any other interactive or automated theorem
provers in this area, to develop my research on using Agda in verification further, but the position below is advertised more broadly (it covers both railway verification and formal methods for cyber security).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Currently we have a job opportunity in applied formal methods at Swansea University, see<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://www.swansea.ac.uk/jobs-at-swansea/current-vacancies/details/?nPostingID=135966&nPostingTargetID=168494&ID=QHUFK026203F3VBQB7VLO8NXD&lg=UK&mask=suext">https://www.swansea.ac.uk/jobs-at-swansea/current-vacancies/details/?nPostingID=135966&nPostingTargetID=168494&ID=QHUFK026203F3VBQB7VLO8NXD&lg=UK&mask=suext</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I was thinking about leaders in Formal Methods, who also have applications in their view. Here your name came to my mind.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">It might be that the deadline will be extended in the course of next week, but since I'm away I wanted to draw your attention to this opportunity now.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Our department hosts one of the UK’s largest groups in logic and theoretical computer science. Furthermore, there is a newly founded, active group on cyber-security. Overall, the department offers a vibrant research environment, also with
experts in AI, HCI, Robotics, and Visual Computing.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Links:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://www.swansea.ac.uk/compsci/research-and-impact/swansea-railway-verification/">https://www.swansea.ac.uk/compsci/research-and-impact/swansea-railway-verification/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://www.swansea.ac.uk/compsci/research-and-impact/theoretical-computer-science/">https://www.swansea.ac.uk/compsci/research-and-impact/theoretical-computer-science/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://www.swansea.ac.uk/compsci/research-and-impact/cybersecurity/">https://www.swansea.ac.uk/compsci/research-and-impact/cybersecurity/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://www.swansea.ac.uk/compsci/research-and-impact/">https://www.swansea.ac.uk/compsci/research-and-impact/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">In case you know of any suitable person, I would be happy if you could point them towards this opportunity. I will be available for an informal chat on Swansea perspectives (from Monday 11 September when I'm back from my current trip).<o:p></o:p></p>
<p class="MsoNormal"><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Best wishes,<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Anton<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div id="divtagdefaultwrapper">
<div id="divtagdefaultwrapper">
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">-----------------------------------------------------------------------------<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Dr Anton Setzer<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Darllenydd / Reader<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Ystafell / Room 403<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Adran Gyfrifiadureg / Dept. of Computer Science<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Y Ffowndri Gyfrifiadurol / Computational Foundry<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Coleg Gwyddoniaeth / College of Science<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Prifysgol Abertawe/ Swansea University<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Campws y Bae/ Bay Campus<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="DE" style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Abertawe / Swansea SA1 8EN<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="DE" style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">DU / UK<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="DE" style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Rhowch wybod i ni os hoffech dderbyn eich gohebiaeth yn Gymraeg. / Let us know if you would like to receive correspondence in Welsh.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Rydym yn croesawu gohebiaeth yn Gymraeg neu yn Saesneg. / We welcome correspondence in Welsh or English.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB">Ni fydd gohebu yn Gymraeg yn arwain at oedi./ Corresponding in Welsh will not lead to a delay.
<o:p></o:p></span></p>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB"><o:p> </o:p></span></p>
</div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black;mso-ligatures:none;mso-fareast-language:EN-GB"><o:p> </o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>