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 werden die konzeptionelle Komplexität durch die Anwendung kompositioneller Ansätze verringern. Konkret werden die kompositionellen Ansätze Entwurfsmuster aus dem Reengineering ausnutzen. Wir werden ein Portfolio an kompositionellen Resultaten entwickeln, welche es ermöglichen werden, 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 werden unseren Ansatz und unsere Resultate anhand von realistischen Programmen evaluieren, inklusive der HPC-Applikationen von Teilprojekt P.
PPK Workflow
Sie sollten einen soliden Hintergrund in mindestens einem der folgenden Bereiche haben:

  • Formale Methoden in Informatik oder Mathematik
  • Semantik von nebenläufigen Programmen oder schwachen Speichermodellen
  • Programmanalyse oder Transformationstechniken
  • Nutzung von Verifikationstools wie Isabelle/HOL oder Coq
Deutsch