Formal verification and testing for concurrent software

A concurrent program can pass thousands of tests and still fail under a thread schedule that nobody anticipated. Weak memory and subtle synchronization make these failures difficult to reproduce—and even harder to rule out.

We develop algorithms for detecting races, predicting bugs from observed executions, and directing testing toward unexplored behaviors. Alongside these tools, we study verification methods and the semantics of concurrent languages, connecting practical bug discovery with rigorous guarantees of correctness.

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