The overall objective of this PhD position is the development and application of formal methods to actual software.  Of particular interest are the mainstream libraries of  the  popular programming language Java. These libraries are widely used and therefore their correctness is of the utmost importance.

This research builds on and extends the successful  verification  by means of the  interactive theorem prover KeY of  executable Java versions of Counting sort and Radix sort.

A recent attempt to verify the Java implementation of the TimSort hybrid sorting algorithm as provided by the Java Collections Framework (and which is designed to perform well on real world data) revealed a fundamental error which for certain inputs crashed the software.

In close collaboration with the Software Engineering group of TU Darmstadt,  we succeeded in the verification of the corrected software.  Motivated by this success our overall goal is the systematic verification of the Java Collections Framework. 

As a PhD you will contribute to the realization of this ambitious goal by a further development of the  interactive theorem prover KeY,  which is required to master the complexity of correctness proofs, and the application of the interactive theorem prover KeY to the Java Collections Framework.

You will perform these tasks in close collaboration  with internationally recognized experts  of the  following research groups: Leiden Institute of Advanced Computer Science, Informatics department of the Open University of the Netherlands, Software Science of the Radboud University, and with the Software Engineering group of TU Darmstadt.

Candidates are required to have a Master’s degree in Computer Science  or Mathematics with Compuer Science as subdiscipline, and a specialization in theoretical computer science and formal methods. Preferable qualifications for candidates include proven research talent, an excellent command of English, and good academic writing and presentation skills.

The terms of employment are in accordance with the Dutch Collective Labour Agreement for Research Centres ("CAO-onderzoeksinstellingen"). The initial labour agreement will be for a period of 18 months. After a positive evaluation, the agreement will extended by 30 months. The gross monthly salary, for a PhD student on a full time basis, is €2,246 during the first year and increases to €2,879 over the four year period.

Employees are also entitled to a holiday allowance of 8% of the gross annual salary and a year-end bonus of 8.33%. CWI offers attractive working conditions, including flexible scheduling and help with housing for expat employees.

Please visit our website for more information about our terms of employment: www.cwi.nl/terms-of-employment.

Centrum Wiskunde & Informatica (CWI)

Centrum Wiskunde & Informatica (CWI) is the Dutch national research institute for mathematics and computer science and linked to the Netherlands Organisation for Scientific Research (NWO). The mission of CWI is to conduct pioneering research in mathematics and computer science, generating new knowledge in these fields and conveying it to trade, industry, and society at large.

CWI is an internationally oriented institute, with 160 scientists from approximately 27 countries. The facilities are first-rate and include excellent IT support, career planning, training, and courses.

CWI is located at Science Park Amsterdam that is presently developing into a major location of research in the natural sciences in The Netherlands, housing the sciences of the University of Amsterdam and of the Vrije Universiteit as well as several other national research institutes next to CWI. 

http://www.cwi.nl

Formal Methods group

In the Formal Methods group, our research involves finding solutions to highly pragmatic real-world problems by reducing their complexity through the elegance and beauty of mathematics. Our work yields technological foundations that underpin software engineering and service-oriented computing. With everything we do, we aim to add stability and reliability to those foundations and so to the third-party applications built on them. In this way, we cut the costs of technological failure for business and society and make life easier for programmers, developers and ultimately users. Our no-nonsense approach relies on the smooth transfer of knowledge between senior and junior researchers, reaching back through our rich history as one of CWI’s original research groups. Our work is grounded in our collaborations with partners in business and industry.