Verification of Important Data Structures of the JDK

Typ:	BA
Datum:	2022-01-01
Betreuer:	Mattias Ulbrich
Aushang:

Background

The Java API (aka the "Java Development Kit") contains a number of very central classes implementing important data structures and algorithms on them. The question is: Are they correctly implemented?

KeY is a theorem prover for that allows full functional verification of sequential Java and Java Card programs. Properties can be specified in the Java Modelling Language (JML) or in Java Dynamic Logic. KeY is actively (co-)developed at our group.

KeY has already been used to verify a number of algorithms and data structures from the JDK (e.g. a sorting routine and a hash table implementation). It even uncovered a crucial bug in the TimSort sorting routine implemented in Java.

Goal

It is the goal of this thesis to prove the correctness of a data structure from the JDK and the algorithms that belong to it.

Task

Your task is to specify and verify a central data structure and the algorithms within the class using the specification language JML and to prove them correct using the KeY verification engine.

Amongst the classes that are of interest are: BigInteger, BitSet, ArrayList, ...

Your Profile

Basic knowlegde of predicate logic, specification and calculi, as e.g. taught in the Formal Methods (Formale Systeme) course at KIT, is required.