Java PathFinder: going to Mars without bugs and deadlocks

Modern developers cannot avoid concurrency in their everyday life: they have to build scalable and efficient systems and, eventually, debug them. Which, sometimes, appears to be quite a challenging task.

In the talk, we will discuss one of the existing tools that may help a developer find subtle concurrency issues: Java PathFinder. It is a research JVM that tries to apply model checking to verify that your Java code does not have a problem with deadlocks or data races.

While the major part of the talk is devoted to the tool itself (what are the use cases and limitations), we will also try to put this framework in the overall picture: how does it compare with JCStress and Lincheck.