Java Pathfinder
Recently, Simon Doherty gave a short talk on using Java Pathfinder to find bugs in Java programs. Java Pathfinder is a model checker for Java code, particularly suited to reasoning about multi-threaded code and finding concurrency bugs. Roughly speaking, it searches through all of the different possible execution traces for a given piece of Java Bytecode. Different traces arise from the different possible schedules for executing threads. To do this, Java Pathfinder executes the Java Bytecode in a controlled fashion which allows it to go back and restart from different points with a different schedules. You have to provide some input, so it is really executing the code, rather than using symbolic execution.
The reason Simon got interested in Java Pathfinder is simply that he had a concurrency bug that needed fixing. Having never used it before, he managed to get it going fairly quickly and also find his bug — which really got him thinking that this was a useful tool.
Anyway, I’m not going to say too much more about it, since I haven’t looked more in detail yet. But, it seems like a very impressive project, and definitely worth checking out.