<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Please feel free to further disseminate this announcement and forward it to whomever would be interested.<br class=""><br class=""><div class="">Online version: <a href="https://distrinet.cs.kuleuven.be/jobs/#program_verification" class="">https://distrinet.cs.kuleuven.be/jobs/#program_verification</a><br class=""><br class=""><b class="" style="font-size: 14px;">PhD Positions in Program Verification</b><div class=""><br class="">We have two open PhD student positions in the program verification group. These positions involve performing research on program verification under the supervision of Prof. dr. Bart Jacobs and postdoctoral researcher Amin Timany, with the goal of obtaining a PhD within four to five years. PhD students are expected to publish and present their results regularly at competitive international conferences and journals, which generally involves international travel, as well as to contribute to the Department's educational obligations. Possible topics include:<br class=""><br class=""><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Logical techniques known as "logical relations" for proving properties of advanced programming languages and programs written in those languages, such as compiler correctness, compiler security, correctness of optimizations.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Developing advanced program logics for reasoning about correctness of higher-order programs with fine-grained concurrency.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Developing supporting theories, such as type theory and category theory, to serve as logical and semantic foundations for program logics<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Developing supporting tools, such as proof assistants (e.g. Coq, Agda) and program verification tools (e.g. Iris, VeriFast), including advancing their usability by developing improved automation technologies.<br class=""></div><div class=""><br class=""></div>Links:<br class=""><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Coq: <a href="https://coq.inria.fr" class="">https://coq.inria.fr</a><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Iris: <a href="https://iris-project.org" class="">https://iris-project.org</a><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• VeriFast: <a href="https://github.com/verifast/verifast" class="">https://github.com/verifast/verifast</a><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Prof. dr. Jacobs: <a href="https://distrinet.cs.kuleuven.be/people/bartj" class="">https://distrinet.cs.kuleuven.be/people/bartj</a><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Dr. Timany: <a href="https://distrinet.cs.kuleuven.be/people/amin" class="">https://distrinet.cs.kuleuven.be/people/amin</a><br class=""></div><div class=""><br class=""></div>Profile:<br class=""><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Strong background in computer science (Master's degree or equivalent)<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>• Strong background in mathematical logic and/or theoretical foundations of computer science<br class=""></div><div class=""><br class=""></div>Interested? Contact Prof. Bart Jacobs (<a href="mailto:bart.jacobs@cs.kuleuven.be" class="">bart.jacobs@cs.kuleuven.be</a>) & Dr. Amin Timany (<a href="mailto:amin.timany@cs.kuleuven.be" class="">amin.timany@cs.kuleuven.be</a>) no later than September 30, 2018. Do not hesitate to contact us if you have any questions regarding these open positions.</div></div></body></html>