<html 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=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@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-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
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;}
/* List Definitions */
@list l0
{mso-list-id:277224024;
mso-list-type:hybrid;
mso-list-template-ids:-800288612 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:490799352;
mso-list-type:hybrid;
mso-list-template-ids:-750719306 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l2
{mso-list-id:1100224334;
mso-list-type:hybrid;
mso-list-template-ids:-1784092640 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l2:level1
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l2:level4
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l2:level7
{mso-level-number-format:bullet;
mso-level-text:ï‚·;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style>
</head>
<body lang="en-NL" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">We are looking for a PhD candidate for a 4-year project on Formal Methods for Embedded Systems, as part of SAVES (ScAlable Verification of industrial Embedded control Systems), a collaboration with the University of Münster (WWU Münster).
You will be working on the SAVES project, carried out in collaboration with prof. dr. Paula Herber (University of Twente / WWU Münster).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The overall goal of SAVES is to investigate methods and tools to establish correctness of embedded systems. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily
increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development
process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal
verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and
tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for
industrial embedded systems.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The PhD candidate hired at the University of Twente will be supervised by Marieke Huisman and Paula Herber and will work on extensions of the methods and tools developed in the FMT group for embedded systems, in close collaboration with
the Embedded Systems group in Münster.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">For further information about the group, <span lang="EN-US">
see https://www.utwente.nl/en/eemcs/fmt/</span>. For further information about the project,
<span lang="EN-US">see <a href="https://www.utwente.nl/en/eemcs/fmt/research/projects/saves/">
https://www.utwente.nl/en/eemcs/fmt/research/projects/saves/</a></span>.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">YOUR PROFILE<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l2 level1 lfo1">You have a MSc degree in Computer Science (or equivalent);<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l2 level1 lfo1">You have a thorough theoretical background and a demonstrable interest in embedded or cyber-physical systems, and ideally some prior experience with embedded systems design, formal
methods, and/or interactive theorem provers;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l2 level1 lfo1">You are an enthusiastic student, skilled in exact and abstract thinking;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l2 level1 lfo1">You are proficient in English on an academic level.<o:p></o:p></li></ul>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">OUR OFFER<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The terms of employment are in accordance with the Dutch Collective Labour Agreement for Universities (CAO) and include:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">A fulltime PhD position for four years, with a qualifier in the first year;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">Full status as an employee at the UT, including pension and health care benefits;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">The salary will range from € 2.395 (1st year) to € 3.061,- (4th year) per month, plus a holiday allowance of 8% and a year-end bonus of 8.3%;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">A solid pension scheme;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">Excellent facilities for professional and personal development;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2">A green and lively campus, with lots of sports facilities and other activities.<o:p></o:p></li></ul>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US">INFORMATION AND APPLICATION<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Are you interested in this position? Please send your application via https://www.utwente.nl/en/organisation/careers/!/2021-425/phd-position-on-embedded-systems- before 5th of July and include:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo3">A cover letter (explaining your specific interest and qualifications);<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo3">A detailed Curriculum Vitae;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo3">A list of all courses + marks and a short description of your MSc thesis;<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo3">References (contact information) of two scientific staff members.<o:p></o:p></li></ul>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The deadline of application is July 5, 2021 or until the position is filled. Starting date of the position is as soon as possible, or to be discussed.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">For further information, you can contact Prof.dr.ir. Paula Herber: https://www.uni-muenster.de/EmbSys/team/herber/ or Prof.dr. Marieke Huisman:
<a href="https://wwwhome.ewi.utwente.nl/~marieke/">https://wwwhome.ewi.utwente.nl/~marieke/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">DEPARTMENT<o:p></o:p></span></p>
<p class="MsoNormal">In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. Our central goal is to increase the reliability of the software that we rely on,
as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. The FMT group also participates in the Digital Systems Institute (DSI).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Our institute was ranked first at the most recent research national assessment.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">ORGANIZATION<o:p></o:p></span></p>
<p class="MsoNormal">The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in
almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and
connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands
and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">As an employer, the EEMCS Faculty offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With our Faculty, you will be part of a leading tech university that is changing
our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customizable conditions.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-US">UNIVERSITY OF TWENTE (UT)<o:p></o:p></span></p>
<p class="MsoNormal">University of Twente (UT) has entered the new decade with an ambitious, new vision, mission and strategy. As ‘the ultimate people-first university of technology' we are rapidly expanding on our High Tech Human Touch philosophy and the unique
role it affords us in society. Everything we do is aimed at maximum impact on people, society and connections through the sustainable utilisation of science and technology. We want to contribute to the development of a fair, digital and sustainable society
through our open, inclusive and entrepreneurial attitude. This attitude permeates everything we do and is present in every one of UT's departments and faculties. Building on our rich legacy in merging technical and social sciences, we focus on five distinguishing
research domains: Improving healthcare by personalised technologies; Creating intelligent manufacturing systems; Shaping our world with smart materials; Engineering our digital society; and Engineering for a resilient world.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">As an employer, University of Twente offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With us, you will be part of a leading tech university that is changing our world
for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customisable conditions.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>