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.”