Static Analysis of mixed-granularity Locking Schemes using Abstract Interpretation

As part of a seminar about static race detection tools at the Institute of Theoretical Computer Science at TU Braunschweig, I spent a semester learning about the Goblint static analysis tool and the theoretical foundations it uses to reason about the semantic space of a program, specifically concurrent low-level C programs in the context of Linux kernel device driver software. This is a paper that I wrote that mainly references the work of Vojdani et al., but explores a lot more of the surrounding theory. This paper is about their work and other articles that were either previous installments or provide supplementary context. I think it is a good introduction for people into this part of program verification.

Even though this paper is in the standardized ACM format, this work was and will never be published anywhere, because it is not based on my own work. Still, I figured that it might be interesting to know for people what I am working on/learning about at the moment, so I decided to post it here.