Verifikation paralleler Programme für schwache Speichermodelle II

• Antragstellerin: Professorin Dr. Heike Wehrheim
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Informatik
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 467386514

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 beeinflussen. 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 spezielle Speichermodelle transferiert. In der zweiten Laufzeit des Projektes werden wir uns dabei auf Lebendigkeitseigenschaften sowie auf Fragen der Robustheit von Programmen bezüglich Speichermodellen konzentrieren.

• DFG-Verfahren: Sachbeihilfen