Concurrency

Concurrent programs must behave correctly across many possible interactions between threads and processes. Bugs can depend on rare schedules, subtle synchronization patterns, or the memory model of the underlying language and hardware. We develop algorithms and tools that make these behaviors easier to explore, understand, and verify.

Our work connects the mathematical foundations of concurrency with practical program analysis. We study both the complexity of verification problems and techniques that scale to real executions.

Research directions

  • Memory models and language semantics. Understanding weak memory and message-passing concurrency, and developing rigorous semantics for concurrent programming languages such as Go.
  • Testing, runtime verification, and predictive analysis. Finding concurrency bugs through fuzzing and schedule exploration, monitoring correctness conditions such as linearizability, and predicting errors from observed executions.
  • Formal verification. Developing proof techniques and automated methods for establishing the correctness of concurrent programs and distributed protocols.

Selected publications

All projects