Zertifizierende Algorithmen für interaktive Komponenten und verteilte Systeme

Ein zertifizierender Algorithmus produziert bei jeder Berechnung zusätzlich zum Resultat noch einen Zeugen, der die Korrektheit des Resultats zeigt. Im besten Fall ist der Zeuge unmittelbar verständlich. Andernfalls überprüft ein (vergleichsweise einfacher) Checker-Algorithmus den Zeugen. Seit den 2000er Jahren werden für zahlreiche "klassische" Algorithmen zertifizierende Varianten entwickelt. Rechnerintegrierte Systeme sind heutzutage oft aus interaktiven Komponenten aufgebaut, die als Knoten eines verteilten Systems lose gekoppelt miteinander interagieren. Algorithmen für interaktive Komponenten terminieren im Allgemeinen nicht. Weiterhin kennen die Komponenten eines verteilten Systems meist nicht die vollständige Struktur des Systems. Algorithmen für solche Komponenten und Systeme verhalten sich entsprechend prinzipiell anders als klassische Algorithmen. In diesem Projekt wird untersucht, wie weit die Idee der Zertifizierung bei Algorithmen für interaktive Komponenten und verteilte Systeme trägt. Das ist deshalb besonders interessant, weil Algorithmen für interaktive Komponenten und verteilte Systeme komplizierter sind als klassische Algorithmen und deren formale Verifikation weit über den derzeitigen Stand der Technik hinausgeht.