PhD position: Decision Procedures for Inductive Separation Logic Modulo Data Theories
The goal of this PhD project is to devise 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 theory reasoning based on external tools (to take into account the properties of the data stored inside the structure).
View online : http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf
