Writing concurrent algorithms correctly is difficult. Common testing techniques do not help much in the context of concurrent programs, owing to the non-deterministic behaviors of these programs and the fact that some bugs can only manifest in a specific environment (for example, in the relaxed memory model of particular hardware).

Model checking is a formal verification technique that helps uncover bugs in concurrent programs by systematically exploring various execution traces of a program in a controlled environment.

In this project, we’re developing novel techniques to tackle this problem, trying to improve existing model checking tools for concurrent programs, and field-testing them on real-world software projects.