[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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:[email protected]
<mailto:[email protected]>> (LIG) and Radu Iosif
<mailto:[email protected]
<mailto:[email protected]>>(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:[email protected]
<mailto:[email protected]>> and
<mailto:[email protected]
<mailto:[email protected]>>
Starting date: October 1st 2021
