Why use VJP?

Why should I verify/state-model check? This question is best answered by the The Java PathFinder Team . But in short, verifying can find possible unhanded exceptions and deadlock situations right out of the box. With further configuration, JPF can be used to detect the possibility of any other more specific situation.

Can JPF verify my program? Once again, probably best answered by the The Java PathFinder Team . The quick answer is that JPF can verify any program that doesn't rely on native code that is not implemented by JPF. Other than that JPF is limited by memory.

I already use JPF just fine, why should I use VJP? VJP can help you manage your configuration files. With a built in mode property configuration editor, and colored syntax editing the files becomes much easier. VJP is also integrated with your project, so that setting things like the classpath are done automatically. (No need to go through all of your files just to add an entry, VJP takes care of that for you.) Besides that, VJP isn't just a configuration file editor, it is also a powerful JPF listener. VJP doesn't just show the results of JPF, it also displays its own graphical representation JPF's results. So that a real picture of the state and execution path can be formed.