TP-K: Skalierung durch Zerlegung

Das Ziel von Teilprojekt K ist die Verbesserung der Skalierbarkeit der Verifikation von Programmen, welche durch Reengineering entstanden sind. Wir verringern die konzeptionelle Komplexität durch die Anwendung kompositioneller Ansätze. Konkret nutzen wir die kompositionellen Ansätze Entwurfsmuster aus dem Reengineering. Wir entwickeln ein Portfolio an kompositionellen Resultaten, welche es ermöglichen, Garantien für ein komplexes Programm aus Eigenschaften von dessen Komponenten herzuleiten. Formale Semantik und Verifikation werden eingesetzt, um eine hohe Zuverlässigkeit der Resultate zu erreichen. Rely-guarantee Techniken werden verwendet, um eine hohe Präzision der kompositionellen Ansätze sicherzustellen. Wir evaluieren unseren Ansatz und unsere Resultate anhand von realistischen Programmen, inklusive der HPC-Applikationen von Teilprojekt P.