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).


Contact | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4181381