Abstract
JPF-static is an extension for Java Pathfinder, which combines exhaustive state space traversal and dynamic analysis with static analysis. The main purpose of JPF-static is efficient and scalable verification of multi-threaded programs in Java.