In testing theory, we are looking to write algorithms for testing software against a model of that software. A testing algorightm generates test sequences based on a labeled transition system model, in such a way that we are sure that - eventually - all behavior of the system gets tested.
In semi-automated theorem proving, we formalize mathematical theorems and show they are correct using software that rigorously checks every step in the proof. Preparing a mathematical theorem to be checked requires mathematical skills, in particular understanding of set theory and type theory, and programming skills, in particular insight in term-rewriting. A theorem prover like LEAN4 is able to automatically derive some steps in a proof, but still requires the outline of a proof to be quite detailed.
Formalising the theory of labeled transition systems, and proving correctness of testing algorithms, is expected to give us new insights in the theory, as it often uncovers hidden assumptions. It also often helps to clean up definitions and improve the didactics when explaining the theory. Furthermore, we also see this as an exercise in formalization, which gives us insight in how semi-automated theorem proving works, which mechanisms of LEAN4 are effective and which ones are not, and how semi-automated theorem provers may be improved in the future.
If you get engaged in this project, it will change your view on mathematics as well as on programming, and you'll learn some testing theory as well on the go.
Contact: Pieter Cuijpers and Michail Karatarakis.