Weak memory models describe the behaviour of concurrent programs on multicore architectures. C11 is the 2011 standard of C which comes with a memory model for the language itself (not for the hardware). Based on the semantics of C11 specified in [1], the purpose of the master thesis is to
(a) develop an interpretation of the program logic Piccolo recently introduced in [2] and
(b) develop proof rules for reasoning about C11 programs (more specifically, the memory triples of [2]).

[1] Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim: Owicki-Gries Reasoning for C11 RAR. ECOOP 2020: 11:1-11:26.
[2] Ori Lahav, Brijesh Dongol, Heike Wehrheim: Rely-Guarantee Reasoning for Causally Consistent Shared Memory. CAV (1) 2023: 206-229.

Spass am Arbeiten mit theoretischen Formalismen; sehr gute Kenntnisse in Logik und Grundlagen der theoretischen Informatik.