Zum Inhalt

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. Frantisek Farka Senior Researcher

Dr. Shuanglong Kan Senior Researcher

Dr. Sara Zain Senior Researcher

Carmine Abate Associate Researcher

M. Sc. Marcus Rossel Research Associate

Dipl.-Inf. Lisza Zeidler Associate Researcher

Max Kurze Associate Researcher

Prof. Dr. Jeronimo Castrillon BI Research Fellow

Publications

Sebastian Ertel, Max Kurze, Michael Raitza, On the Potential of Coq as the Platform of Choice for Hardware Design, Coq Workshop, 2024

Link to PDF

@inproceedings{
ertelCOQ2024,
title = "On the Potential of Coq as the Platform of Choice for Hardware Design",
author = "Sebastian Ertel, Max Kurze, Michael Raitza",
year = "2024",
booktitle = "Coq Workshop",
url = "https://coq-workshop.gitlab.io/2024/files/EA4.pdf"
}
Download BibTex
Zum Seitenanfang