Verified System Design Automation
The Verified System Design Automation group (VerSA) focuses on ensuring trustworthiness “by design” in hardware and software systems through formal verification and formally verified compilation.
Verification
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.
Automation
Theorem proving and mathematical reasoning often require a high level of expert knowledge, which impedes their integration into the conventional development cycle. To overcome this problem, we identify domains where all programs have common properties. Example domains are hardware designs for scalable multi-processor systems and distributed programs for micro-kernel operating systems. For such domains, we create domain-specific languages and compilers. Our compilers establish important properties across the software and hardware stack. Developers can use them to design hardware or distributed programs without requiring theorem proving expertise.
Who we are
Dr.-Ing. Sebastian Ertel Research Group Leader
Dr. Carmine Abate Senior Researcher
Dr. Frantisek Farka Senior Researcher
Dr. Shuanglong Kan Senior Researcher
Dr. Sara Zain Senior Researcher
Dipl.-Inf. Max Kurze Associate Researcher
B.Sc. Mohamed Abdelhameed Elsheikh Student Assistant
B.Sc. Kleio Liotati Student Assistant
B.Sc. Matthias Meißner Student Assistant
B.Sc. Amr Yonis Student Assistant
Prof. Dr. Jeronimo Castrillon BI Research Fellow
