PhD Student on the subject of Verification of Mainstream Java Libraries

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.