<div dir="ltr"><div class="gmail_quote gmail_quote_container"><div dir="ltr"><div class="gmail_quote"><div dir="ltr"><p class="MsoNormal" style="margin:0in 0in 6pt;line-height:normal;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;font-family:"Times New Roman",serif;color:rgb(5,5,5)">Open PhD positions in the
department of Computer Science and Engineering at Chalmers University of
Technology / the University of Gothenburg, Sweden. The students will work with </span><span style="font-size:12pt;font-family:"Times New Roman",serif;color:rgb(5,5,5)">Professor Nir Piterman in the formal methods unit.</span></p><p class="MsoNormal" style="margin:0in 0in 6pt;line-height:normal;font-size:11pt;font-family:"Calibri",sans-serif"><span style="color:rgb(5,5,5);font-family:"Times New Roman",serif;font-size:12pt">These positions are supported by WASP - the Wallenberg AI, Autonomous Systems, and
Software Program.</span></p>

<p class="MsoNormal" style="margin:0in 0in 6pt;line-height:normal;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;font-family:"Times New Roman",serif;color:rgb(5,5,5)">Research scope: formal verification,
reactive synthesis, planning, automata, games, temporal logics<span></span></span></p>

<p class="MsoNormal" style="margin:0in 0in 8pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;line-height:107%;font-family:"Times New Roman",serif">Apply
here: </span><a href="https://tiny.cc/gbgphd" style="color:blue;text-decoration:underline" target="_blank">https://tiny.cc/gbgphd</a><span></span></p>



<p class="MsoNormal" style="margin:0in 0in 6pt;line-height:normal;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;font-family:"Times New Roman",serif">The successful candidates will work on combinations of formal verification and planning on symbolic AI that is used in reinforcement learning and directly in robotics and reactive software development. <span></span></span></p>

<p class="MsoNormal" style="margin:0in 0in 6pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;line-height:107%;font-family:"Times New Roman",serif">More concretely, the work will include the
study of temporal logic, planning domains and planning techniques, automata,
and two player games. Temporal logic and planning domains are used for symbolically describing in a high level the world surrounding a program, planning
techniques are used to extract information about the problem, automata are used
as an algorithmic tool for manipulation of logic formulae, and two-player games
enable to consider strategies and programs. We will study these formalisms,
analyze their properties, devise algorithms to manipulate and translate between
them, as well as implement tools that will show the applicability of the
developed techniques. <span></span></span></p>

<p class="MsoNormal" style="margin:0in 0in 6pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-family:"Times New Roman",serif;font-size:12pt">PhD (third-cycle) education is through a
fixed-term employment contract for 5 years. During these 5 years, most of the
student’s time will be devoted to their research. They will also be assisting
the department’s education by working 20% of their time on a teaching or supporting
role. The 20% support component may be concentrated in certain parts of the
year according </span>to the department's<span style="font-family:"Times New Roman",serif;font-size:12pt"> needs (in consultation with the student). In
addition, the student will have to undertake 60 Higher Education Credits (HECs)
in courses enriching their knowledge in computer science, supporting their
research, and gaining general (scientific) skills.</span></p>

<p class="MsoNormal" style="margin:0in 0in 6pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"><span style="font-size:12pt;line-height:107%;font-family:"Times New Roman",serif">This project is supported by WASP and the
appointed student will also belong to the WASP graduate school. Some of the
required HECs will be specialized WASP courses about autonomous systems and AI.
The appointed student will also be eligible to participate in other WASP supported
programs (such as visits to universities abroad or short-term research visits
to other universities). <span></span></span></p>





<br></div>
</div></div>
</div></div>