[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The research group Formal Methods and Tools at the University of Twente (Enschede - The Netherlands) is looking for a PhD researcher (4 years) and a post doc researcher (3 years), to work on the 5 year research project VerCors (Verification of Concurrent Data Structures), funded by the European Research Council. The PhD student will work in particular on: The specification and Verification of Concurrent Data Structures with different Locking Policies The post doc researcher will work in particular on: User-friendly specification and automated verification of concurrent data structures Our research: ------------- Goal of the VerCors project is to develop a general specification and verification technique for multithreaded software. In earlier work, we developed a variant of permission-based separation logic that is particularly suited to reason about multithreaded Java programs with dynamic thread creation and termination, and reentrant locks. Expressiveness of this logic will be extended, to specify and verify different concurrent data structures. The PhD student will work on the parametrisation of the verification logic over the locking policy, so that a high-level specification of the behaviour of a data structure can be reused for different implementations. Thus the implementation of a concurrent data structure can be changed, without affecting correctness of the applications using it. The developed technique will be applied on standard concurrency libraries, such as java.concurrency.util. The post doc will be actively involved in the whole project. In addition, he or she is expected to work in particular on the following topics: - the development of an appropriate specification language, combining readability à la JML and expressiveness related with concurrency as in separation logic. - the automated verification of proof obligations, by developing or extending appropriate solvers for separation logic, and developing ownership type-based techniques to prove the absence of aliasing automatically. All results of the VerCors will be integrated in a tool set that generates and proves proof obligations automatically. It will be validated on realistic case studies. For more information about the project, see: http://fmt.cs.utwente.nl/projects/VerCors/ We seek: -------- A PhD student with an MSc degree in Computer Science (or an equivalent qualification) and a post doc with a PhD degree in Computer Science (or an equivalent qualification). The candidate should be enthousiastic, and have a thorough theoretical background, a demonstrable interest in program verification, and some knowledge about multithreaded programming (in Java/C/C++). We are looking for a researcher with an independent mind who is willing to cooperate in our team. It is understood that he or she works on the topics listed above. Further we ask for good communicative and good collaboration skills. Candidates should be prepared to prove their English language skills. As a research outcome we expect publications, (prototype) tools, and for the PhD student a PhD thesis. Starting date of the position: as soon as possible after February 1, 2011. We offer: --------- - A PhD position for four years (38 hrs/week) and a post doc position for three years (38 hrs/week) - A stimulating scientific environment - Gross salary for a PhD student ranging from E 2042 tot E 2612 (4th yr) per month - Post doc salary is dependent on experience and background, but will minimally be EUR 2861 gross per month, plus benefits. - Holiday allowance (8%), end-of-year bonus (8.3%) - Excellent facilities for professional and personal development. - Good secondary conditions, in accordance with the collective labour agreement CAO-NU for Dutch universities - A green Campus with lots of sports facilities The PhD student will be a member of the Twente Graduate School in the research programme 'Dependable and Secure Computing' under the leadership of Prof Dr Jaco van de Pol. The research programme offers advanced courses to deepen your scientific knowledge in preparation to your future career (within or outside academia). We provide our PhD students with excellent opportunities to broaden their personal knowledge and to professionalise their academic skills. Participation in national and/or international summer schools and workshops, and visits to other prestigious research institutes and universities can be part of this programme. Further information: -------------------- - FMT group: http://fmt.cs.utwente.nl/ - Dr. Marieke Huisman (marieke.huis...@ewi.utwente.nl) Application: ------------ Please submit your application via http://www.utwente.nl/vacatures/en/ before December 15th, 2010. However, we strongly encourage interested applicants to send in their applications as soon as possible. Your application should consist of: - a cover letter (explain your specific interest and qualifications); - a full Curriculum Vitae, to apply for the PhD student position, this should include a list of all courses + marks, and a short description of your MSc thesis; to apply for the post doc position, this should include a list of all publications, and a short description of your PhD thesis; - references (contact information) of two scientific staff members.