Java PathFinder is a system to verify executable Java bytecode programs. In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Unlike traditional debuggers, JPF reports the entire execution path that leads to a defect. JPF is especially well-suited to finding hard-to-test concurrency defects in multithreaded programs.
While software model checking in theory sounds like a safe and robust verification method, reality shows that it does not scale well. To make it practical, a model checker has to employ flexible heuristics and state abstractions. JPF is unique in terms of its configurability and extensibility, and hence is a good platform to explore new ways to improve scalability.
JPF is a pure Java application that can be run either as a standalone command line tool, or embedded into systems like development environments. It was mostly developed — and is still used — at the NASA Ames Research Center. Started in 1999 as a feasibility study for software model checking, JPF has found its way into academia and industry, and has even helped detect defects in real spacecraft.
javapathfinder-4.1.947-1.src.rpm
equals, not ==.StringBuffer
effectively. Actually, the original patch has been applied, as well
as numerous other cases of the same thing. This patch now contains
the last several instances that I can see.arraycopy
instead of looping.==.true.