Record #248497 - iMPULSE

DFG project G:(GEPRIS)467386514

Verifikation paralleler Programme für schwache Speichermodelle

Coordinator	Professorin Dr. Heike Wehrheim
Grant period	2021 -
Funding body	Deutsche Forschungsgemeinschaft
	DFG
Identifier	G:(GEPRIS)467386514

Note: 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.

Recent Publications

There are no publications

Record created 2023-01-20, last modified 2024-09-27

Similar records

Rate this document:

(Not yet reviewed)

Add to personal basket
Export as Author List with IDs BibTeX (UTF-8), EndNote XML, EndNote Text, RIS, MARC, Print MARC, MARCXML, DC,
Request correction
Submit fulltext

guest :: login iMPULSE
		Search		Submit		Personalize Your alerts Your baskets Your searches		Help