Die Verified System Design Automation Group (VerSA) konzentriert sich darauf, durch formale Verifikation und formal verifizierte Kompilierung die Zuverlässigkeit von Hardware- und Softwaresystemen von Grund auf sicherzustellen.
In einer digitalen Gesellschaft werden die Systeme zunehmend komplexer. Mit Millionen von Ausführungswegen ist es sehr schwierig, Vertrauen in solche komplexen Systeme aufzubauen. Jeden einzelnen Pfad zu testen, ist praktisch unmöglich und kostet viel Energie. In unserer Gruppe versuchen wir, teure Tests durch mathematische Schlussfolgerungen zu ersetzen. Bereits in der Designphase verwenden wir Theorembeweiser wie Coq, um die Korrektheit der von uns (mit)entwickelten Systeme mathematisch zu beweisen. Diese formale Verifikation stellt sicher, dass unsere Systeme gemäß unseren Erwartungen funktionieren (funktionale Korrektheit) und Sicherheit gegen potentielle Bedrohungen gewährleisten. Somit macht die formale Verifikation unsere Systementwürfe sowohl vertrauenswürdig als auch energieeffizient.
Das Beweisen von Theoremen und das mathematische Argumentieren erfordern oft ein hohes Maß an Expertise, was die Integration in den konventionellen Entwicklungszyklus behindert. Um dieses Problem zu überwinden, identifizieren wir Anwendungsbereiche, in denen alle Programme gemeinsame Eigenschaften haben, z. B. Hardware-Designs für skalierbare Mehrprozessorsysteme und verteilte Programme für Mikrokern-Betriebssysteme. Für solche Bereiche entwickeln wir spezifische Sprachen und Compiler. Unsere Compiler definieren wichtige Eigenschaften für Software und Hardware. Entwickler:innen können sie verwenden, um Hardware oder verteilte Programme zu entwerfen, ohne Fachwissen im Beweisen von Theoremen zu benötigen.
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"
}
