We are seeking an enthusiastic PhD candidate with a strong background
in computer science, software engineering, mathematics, or closely
related fields. Expertise in formal methods such as program reasoning,
programming language semantics, model checking, theorem proving, or
computational logic is essential.
Mathematical models, e.g., describing physical systems or
cryptographic algorithms, rely on ideal numbers. For instance,
mathematical integers are infinite and mathematical reals continuous
and infinite. Computers work with finite approximations that are
bounded (i.e., there is a smallest and largest number) and
discrete. This "digital gap" between mathematical models and actual
systems is a challenge when implementing safety-critical or
security-critical systems: for example, autonomous aircraft or
self-driving cars require high-precision representations of their
position to avoid collisions. Hence, not considering the approximation
of the approximative representation of numbers in computers can result
in crashes that can endanger the life of humans. Moreover, many
security-critical systems, not limited to cryptographic algorithms,
rely on the correct handling of over- and underflows in integer
computations. Actually, underflow- and overflow bugs are a root cause
for a large number vulnerabilities exploited by cyber security
criminal, e.g., for stealing digital currencies worth several billion
of dollars. While this is not a new problem (e.g., already in 1982, an
float conversion error in a trading systems at the Vancouver Stock
Exchange resulted in a loss of several millions of US dollars), an
integrated development method preventing such bugs is still not
available.
This PhD project will address this challenge by developing a rigour
approach for developing systems relying on precise representations of
numbers, using the interactive theorem prover Isabelle/HOL. The PhD
project can focus on
1) the formalisation of concrete representations of machine numbers
(e.g., IEEE754, POSIT, Decimal Floating Point, Fixed Point
Arithmetic), their (algebraic) properties, and relationship to
abstract mathematical numbers;
2) the formalisation and verification of numerical or cryptographic
algorithms, establishing a reusable verified library, or
3) the development of an end-to-end refinement approach from
mathematical models to machine representations.
The PhD will be jointly supervised by Prof. Dr. Achim Brucker
(