An MSO Framework for Weak-Memory Verification and Robustness

Giovanna Kobus Conrado, Andreas Pavlogiannis

Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of thei…