Towards Automation of LTL Verification for Java Pathfinder

Model checking is a powerful and promising technique for software verification. How-ever current model checker is not efficient enough to be used broadly in practice. One of the problem is the ability to verify efficiently rich specifications for sequential pro-grams, formally called the "Specification specific" problem. In this project, the authors' study the "Specification specific" problem for Java Pathfinder, a well-known model checker for Java programming language. The paper implements LTL2JPF Translator to automatically model check LTL specifications for Java programs using Java Pathfinder as the back-end model checker. The paper evaluates LTL2JPF Translator on JavaCup and jDepend project and show that the tool is scalable to complex LTL formulas and Java programs.