<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);">The LIG (<a href="https://www.liglab.fr/" class="">https://www.liglab.fr/</a>) and VERIMAG (<a href="http://www-verimag.imag.fr/" class="">http://www-verimag.imag.fr/</a>) laboratories in Grenoble are seeking an outstanding PhD candidate to fill the following 3-years funded position:</div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);"><br class=""></div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);">Decision Procedures for Inductive Separation Logic Modulo Data Theories</div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);"><br class=""></div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);">Advisors: Nicolas Peltier <<a href="mailto:Nicolas.Peltier@univ-grenoble-alpes.fr" class="">mailto:Nicolas.Peltier@univ-grenoble-alpes.fr</a>> (LIG) and Radu Iosif <<a href="mailto:Radu.Iosif@univ-grenoble-alpes.fr" class="">mailto:Radu.Iosif@univ-grenoble-alpes.fr</a>>(VERIMAG)</div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);"><br class=""></div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);">The goal of this PhD project is to devise decision procedures for
Separation Logic with user-provided inductive definitions of predicates.
We intend to find a procedure that is optimal from a theoretical point
of view, practically efficient, and able to handle a class of
definitions that is as large as possible, combining spatial reasoning
(to reason on the shape of the considered data structures) with data
theory reasoning based on external tools (to take into account the
properties of the data stored inside the structure). Full description: <a href="http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf" class="">http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf</a> </div><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);"><br class=""></div><div class=""><div class="" style="margin: 0px; font-stretch: normal; line-height: normal; color: rgba(0, 0, 0, 0.85);">How to apply: send your CV to <<a href="mailto:Nicolas.Peltier@univ-grenoble-alpes.fr" class="">mailto:Nicolas.Peltier@univ-grenoble-alpes.fr</a>> and <<a href="mailto:Radu.Iosif@univ-grenoble-alpes.fr" class="">mailto:Radu.Iosif@univ-grenoble-alpes.fr</a>></div></div><div class=""><br class=""></div><div class="">Starting date: October 1st 2021</div></body></html>