Concurrency Reasoning for Weak Memory II

• Applicant: Professorin Dr. Heike Wehrheim
• Subject Area: Software Engineering and Programming Languages ; Theoretical Computer Science
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 467386514

Program verification aims at formal proofs of program correctness with respect to specified properties. For parallel programs, correctness does not only depend on the program itself, but also on the memory model of the executing hardware. Many and multi core architectures possess so called weak (or relaxed) memory models which significantly influence the semantics of parallel programs. The objective of this project is the development of a generic verification technique which allows to generate correctness proofs independent of a memory model and is then able to transfer a proof to specific models. In the second phase of our project we will concentrate on liveness properties and the question of robustness of programs against weak memory models.

• DFG Programme: Research Grants