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