Job Description
The goal of this PhD is to develop new methods and tools for program verification using Separation Logic. This is a logical framework suitable for reasoning about the dynamic structures manipulated by real-life imperative programs written in C, Java, etc. Separation Logic supports local and compositional reasoning via built-in logical connectives, which makes it particularly suited to design scalable verification methods.
The job of the PhD candidate is to investigate algorithmic aspects related to the decidability of various fragments of Separation Logic, and integrate these results into a full-fledged verification system.
The duration of the PhD thesis is 3 years, starting early 2015. The student will be based at VERIMAG, Grenoble and will closely cooperate with the partners of the VECOLIB projet. This project will be supervised by Dr. Radu Iosif from CNRS/University of Grenoble. The salary after tax is in the range of 1200-1500 euros/month. Access to the French public healthcare system (health insurance) is included. The University of Grenoble provides affordable student accomodation and free French classes.
Your Profile
Must have an university degree in Computer Science or Mathematics with focus on logic, automata theory and/or programming languages (semantics). Good knowledge of C, OCAML or Java programming is considered a plus, as well as fluent English.
How to apply ?
Send your CV to Radu.Iosif@imag.fr. The CV must contain previously obtained degrees with average grades (on the scale used by the local university) and (when applicable) a list of previous scientific work (publications, software, etc.). If possible, one may attach a list of grades to the email, as well.
