The JAVA+ITP tool for Maude is an experimental tool to prove properties about a subset of Java. The semantics of that subset of Java has been defined in Maude, too. The tool is meant as a proof-of-concept to be extended to a larger set of Java or even another language. It makes use of the ITP tool.
The author is Ralf Sasse who can be contacted for questions about the tool.
You can download a tar containing both the source code of the tool, a version of the ITP extended to work with the tool, and a set of examples here. This version has been tested to run under Maude 2.1.1 which must be downloaded separately. Please see the included README file for a description of the tar contents. The best documentation currently available is the paper draft.