PhD Position in Formalizing Number Systems
We have an open PhD position in Bridging the Gap Between Mathematical Numbers and Software Systems. To fill this position, 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
- 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;
- the formalisation and verification of numerical or cryptographic algorithms, establishing a reusable verified library, or
- 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 and Prof. Dr. Burkhart Wolff, leading to a joint degree from the University of Exeter and the University of Paris-Saclay.
Information about the programme can be found at
- https://www.exeter.ac.uk/study/pg-research/funding/phdfunding/paris-saclay/
- https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay
All applications have to be made via the ADUM system: https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay, latest on the 22nd of March 2026.