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, Madanlal Musuvathi, and Vasu Singh, Verifying Local Transformations of Concurrent Programs, in CC 2010: International Conference on Compiler Construction, Springer Verlag, 25 March 2010
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi, On the Verification Problem for Weak Memory Models, in Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, Inc., 20 January 2010
- 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, Memory Model Safety of Programs, July 2008
- Sebastian Burckhardt and Madanlal Musuvathi, Effective Program Verification for Relaxed Memory Models, no. MSR-TR-2008-12, January 2008
