[TYPES/announce] PhD position in automated reasoning (Grenoble, France)

[Radu Iosif]

The LIG (https://www.liglab.fr/) and VERIMAG (http://www-verimag.imag.fr/ <http://www-verimag.imag.fr/>) laboratories in Grenoble are seeking an outstanding PhD candidate to fill the following 3-years funded position:

Decision Procedures for Inductive Separation Logic Modulo Data Theories

Advisors: Nicolas Peltier <mailto:Nicolas.Peltier at univ-grenoble-alpes.fr <mailto:Nicolas.Peltier at univ-grenoble-alpes.fr>> (LIG) and Radu Iosif <mailto:Radu.Iosif at univ-grenoble-alpes.fr <mailto:Radu.Iosif at univ-grenoble-alpes.fr>>(VERIMAG)

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: http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf <http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf> 

How to apply: send your CV to <mailto:Nicolas.Peltier at univ-grenoble-alpes.fr <mailto:Nicolas.Peltier at univ-grenoble-alpes.fr>> and <mailto:Radu.Iosif at univ-grenoble-alpes.fr <mailto:Radu.Iosif at univ-grenoble-alpes.fr>>

Starting date: October 1st 2021
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210729/51fbd9ed/attachment-0001.htm>