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.
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.
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.
Frantisek Farka, Carmine Abate, Shuanglong Kan, Sebastian Ertel,
Debug, Execute, Verify! Development-Verification Co-Design Made Practical,
Proceedings of the 13th Workshop on Programming Languages and Operating Systems,
2025
@inproceedings{
plos_25_farka_et_al,
title = "Debug, Execute, Verify! Development-Verification Co-Design Made Practical",
author = "Frantisek Farka, Carmine Abate, Shuanglong Kan, Sebastian Ertel",
year = "2025",
booktitle = "Proceedings of the 13th Workshop on Programming Languages and Operating Systems",
address = "New York, NY, USA",
series = "PLOS '25",
publisher = "Association for Computing Machinery",
pages = "51-59"
}
Sara Zain, Jannik Mähn, Stefan Köpsell, Sebastian Ertel,
Formally-verified Security against Forgery of Remote Attestation using SSProve,
Computer Security — ESORICS,
2025
@inproceedings{
remote_attestation_ssprove_2026,
title = "Formally-verified Security against Forgery of Remote Attestation using SSProve",
author = "Sara Zain, Jannik Mähn, Stefan Köpsell, Sebastian Ertel",
year = "2025",
booktitle = "Computer Security — ESORICS",
publisher = "Springer Nature Switzerland",
pages = "463--484"
}
Rudi Schneider, Marcus Rossel, Kœhler Thomas, Andrés Goens, Michel Steuwer,
Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs,
Proceedings of the ACM on Programming Languages,
Proceedings of the ACM on Programming Languages,
2025
@article{
slotted_egraphs_2025,
title = "Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs",
author = "Rudi Schneider, Marcus Rossel, Kœhler Thomas, Andrés Goens, Michel Steuwer",
year = "2025",
journal = "Proceedings of the ACM on Programming Languages",
booktitle = "Proceedings of the ACM on Programming Languages",
address = "New York, NY, USA",
month = "jun",
number = "PLDI",
volume = "9",
publisher = "Association for Computing Machinery",
pages = "1888--1910"
}
Max Kurze,
A Framework for Modular and Compositional Reasoning in Kôika,
2025
@mastersthesis{
max_kurze_msc_thesis,
title = "A Framework for Modular and Compositional Reasoning in Kôika",
author = "Max Kurze",
year = "2025",
school = "Technische Universität Dresden",
month = "March",
url = "https://zenodo.org/records/15073479"
}
Garvit Chhabra,
A formally-verified Network-on-Chip in Coq,
2025
@mastersthesis{
garvit_chabra_msc_thesis,
title = "A formally-verified Network-on-Chip in Coq",
author = "Garvit Chhabra",
year = "2025",
school = "Technische Universität Dresden",
month = "January",
url = "https://zenodo.org/records/15004685"
}
Sebastian Ertel, Max Kurze, Michael Raitza,
On the Potential of Coq as the Platform of Choice for Hardware Design,
Coq Workshop,
2024
@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"
}
