Java Programming Toolkit Source Release
The HP Java Programming Toolkit Source Release contains the
source code for several Java analysis tools. For additional
information concerning the Java Programming Toolkit please
This is the Java front end that ESC/Java and Rcc use. In addition to
parsing and type checking Java, it allows subclasses to extend Java
with annotations, like those in ESC/Java.
Download Javafe here:
The HP Extended Static Checker for Java (ESC/Java)
is a tool that attempts to find common run-time errors in Java
programs by static analysis of the program text.
Download Escjava here:
Houdini is a tool that infers the program annotations used by ESC/Java.
Building it requires the Javafe (see above), Escjava (see above),
and Simplify (see below) envelopes.
Download Houdini here:
This envelope contains the Race Condition Checker for Java
which helps identifies potential race conditions in multithreaded
Java code statically. Building it requires the Javafe envelope (see
Download RCC here:
The HP Research ESC/Java Synchronization Checker (Calvin)
is a static checker for multithreaded Java programs that can check
invariants as well as identify potential race conditions.
Download Calvin here:
This envelope contains the sources for the theorem prover
Simplify, which is used by the ESC/Java and Houdini tools.
Simplify is written in Modula-3, so you need a Modula-3 building
environment, which you can download from the net. The Simplify
envelope contains 4 packages (1 or 2 of which may possibly be part
of your Modula-3 installation already). Simplify add these 4
packages to your Modula-3 environment and build them (using
"m3build", if you use SRC Modula-3).
Download Simplify here: