Sober: Find memory consistency bugs
Sober is a methodology for finding memory consistency bugs in software. Sober has a precise understanding of the x86 memory model and can detect if your programs misbehave (i.e. have non-sequentially-consistent executions) when run on x86. Sober is particularly useful for verifying low-lock code and synchronization primitives.
Publications
- Sebastian Burckhardt and Madanlal Musuvathi, Memory Model Safety of Programs, July 2008
- S. Burckhardt and M. Musuvathi, Effective Program Verification for Relaxed Memory Models, in Computer-Aided Verification (CAV), Springer Verlag, July 2008
- Sebastian Burckhardt and Madanlal Musuvathi, Effective Program Verification for Relaxed Memory Models, no. MSR-TR-2008-12, January 2008
