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.
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"
}