View source for Funded 3-year PhD position in Program Verification

'''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. The student will be based at VERIMAG, Grenoble and will closely cooperate with the partners of the [http://vecolib.imag.fr/index.php/Main_Page 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 and access to the French public healthcare system is included. The University also provides 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.