Difference between revisions of "Funded 3-year PhD position in Program Verification"
| Line 10: | Line 10: | ||
'''Your Profile''' | '''Your Profile''' | ||
| − | Must have an university degree in Computer Science or Mathematics with focus on logic, automata theory and/or programming languages (semantics). | + | 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. |
Revision as of 16:23, 12 December 2014
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 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.
