Verification of Efficient Arithmetic Operations

Typ:	BA
Datum:	2018-06-26
Betreuer:	Mattias Ulbrich
Aushang:

Background

Arbitrary precision integers are an important data type, e.g., for the implementation of many cryptographic protocols. In the JDK, there is a class java.math.BigInteger that realises arbitrary precision integers and many operations on them.

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.

Goal

It is the goal of this thesis to prove the correctness of efficient algorithms implementations contained in the BigInteger class. This includes, e.g., an implementation of Karatsuba multiplication.

Task

Your task is to specify and verify important algorithms within the class java.math.BigInteger using the specification language JML and to prove them correct using the KeY verification engine.

You can build on top of results obtained in an earlier Bachelor's thesis.

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.