Software Verification for Weak Memory via Program Transformation

Jade Alglave, Daniel Kroening, Vincent Nimal +1

Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. We propose a sound tr…