Das Gebiet der Programmverifikation beschäftigt sich mit Beweisverfahren zum formalen Nachweis der Korrektheit von Programmen bezüglich spezifizierten Eigenschaften. Ausschlaggebend für die Korrektheit ist bei parallelen Programmen aber nicht nur das Programm selber, sondern auch das der ausführenden Hardware zugrundeliegende Speichermodell. Many- und Multi-core Architekturen besitzen sogenannte schwache Speichermodelle, die die Semantik von parallelen Programmen signifikant beinflussen. Bisher sind vor allem Beweisverfahren entwickelt worden, die spezifisch für ein solches Speichermodell sind.

Das Ziel des Projektes ist Entwicklung einer generischen Verifikationstechnik, die Korrektheitsbeweise für Programme unabhängig von einem Speichermodell entwickeln kann, und Beweise dann auf Speichermodelle transferiert. Dazu soll die Verifikation auf eine axiomatische Basis gesetzt werden, die das verschiedenen Speichermodellen gemeinsame operationelle Verhalten von parallelen Programmen beschreibt und von den technischen Unterschieden abstrahiert. Auf dieser Basis soll (a) eine Sprache zur Eigenschaftsspezifikation sowie (b) ein Beweiskalkül entwickelt werden. Durch den exemplarischen Nachweis der Gültigkeit dieser Axiome für drei Speichermodelle und die Durchführung einer Reihe von Beweis-Fallstudien wollen wir die Generizität der Verifikationstechnik demonstrieren.