Bastiaan Laarakker
Faculty of Science and Engineering | Bachelor Data Science and Artificial Intelligence
"Formalisation of Timed Systems in Coq"
Bastiaan's elevator pitch
"As the correctness of a mathematical proof can be difficult to verify, there are software tools, called proof assistants, which allow for the development and verification of mathematical statements. In this work, I implement a formalisation of the theory of timed system behaviours in the Coq proof assistant. The behaviour of a system is the set of all possible executions that may occur, and many properties of a system may be defined at this level of abstraction. Implementing this in a proof assistant allows us to verify its correctness and develop the theory further. Finally, my work highlights some features and limitations of Coq and its underlying foundations.”
![Bas_Laarakker](/sites/default/files/2024-01/Bas%20Laarakker.jpg)
Congratulations Bastiaan
In this video Bastiaan is addressed briefly by the immediate supervisor.