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.
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. Amr Yonis Student Assistant
Prof. Dr. Jeronimo Castrillon BI Research Fellow
@inproceedings{
max_typed_binders_rocqPL26,
title = "Scalable Type Inference for Intrinsically-Typed Binders",
author = "Max Kurze, Clément Pit-Claudel, Sebastian Ertel",
year = "2026",
booktitle = "Workshop on Rocq for Programming Languages"
}
@inproceedings{
carmine_wp_prisc26,
title = "WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification",
author = "Carmine Abate, Mohamed Elsheikh, Kleio Liotati, Frantisek Farka, Sebastian Ertel",
year = "2026",
booktitle = "10th Workshop on Principles of Secure Compilation"
}
@article{
kan_string_cpp26,
title = "Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis",
author = "Shuanglong Kan, Anthony Widjaja Lin",
year = "2026",
journal = "Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs",
pages = "279-293"
}
@article{
10.1145/3776667,
title = "Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation",
author = "Marcus Rossel, Rudi Schneider, Kœhler Thomas, Michel Steuwer, Andrés Goens",
year = "2026",
journal = "Proc. ACM Program. Lang.",
month = "January",
number = "POPL",
volume = "10"
}
@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"
}
@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"
}
@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"
}
@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"
}
@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"
}
@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"
}