Sebastian Burckhardt Researcher, Concurrency Research Group Microsoft Research, Redmond, WA e-mail: sb urck ha @ micro soft.c om

Interests

My research interests revolve around algorithms and strategies that simplify the design and verification of concurrent systems on shared memory platforms.

• Shared-memory Multiprocessing
  • Concurrent Data Types
  • Lock-free Synchronization
  • Relaxed Memory Models
  • Cache Coherence Protocols
• Verification (Model Checking), Programming Languages
• Abstraction Techniques, Reductions

Projects

I am currently starting a new project called SoBeR (Store Buffer Race Detector) with Madan Musuvathi. Prior to joining Microsoft, I developed a verification tool called CheckFence as part of my PhD research.

Publications

• S. Burckhardt, M. Musuvathi. Effective Program Verification for Relaxed Memory Models. Computer-Aided Verification (CAV 2008).
• S. Burckhardt, M. Musuvathi. Memory Model Safety of Programs. Workshop on "Exploiting Concurrency Efficiently and Correctly" (EC^2 2008).
• S. Burckhardt. Memory Model Sensitive Analysis of Concurrent Data Types. Doctoral Dissertation (University of Pennsylvania, August 2007).
• S. Burckhardt, R. Alur, M. Martin. CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. Programming Language Design and Implementation (PLDI 2007).
• S. Burckhardt, R. Alur, M. Martin. Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. Computer-Aided Verification (CAV 2006).
• S. Burckhardt, R. Alur, M. Martin. Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement. Verification, Model Checking and Abstract Interpretation (VMCAI 2005).
  

---