Under this umbrella project, we’re working on model-checking tools that help uncover sophisticated bugs in concurrent programs.
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.