Parameterized Static Analysis for Weak Memory Models

Verifying programs under weak memory models (WMMs) is vital due to their prevalence in modern computer architectures. These models introduce complexities, allowing unexpected reordering and visibility of memory operations. Ensuring correctness is crucial to prevent subtle bugs and guarantee the reliability of software running on such systems. However, a memory model specific technique cannot be extended to other memory models. In this work, we strive to develop an automated parameterized verification technique capable of analyzing programs under all possible WMMs.