The systems in a digital society are increasingly complex. With millions of execution paths, it is extremely difficult to establish trust in such complex systems. Testing every single path is practically unfeasible and energy intensive.
In our group, we aim to replace expensive testing with mathematical reasoning. As early as during design time, we use theorem provers such as Coq to mathematically prove the correctness of the systems that we (help to) develop. This formal verification ensures that our systems operate according to our expectations (functional correctness) and preserve security against potential threats. As such, formal verification makes our system designs both trustworthy and energy efficient.