ESC/Java2 Summary
The Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts to find common run-time errors in JML-annotated Java programs by static analysis of the program code and its formal annotations. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with specially formatted comments called pragmas.
ESC/Java2 is available in three forms.
- ESC/Java2 is built into the MOBIUS Program Verification Environment
- ESC/Java2 is a command-line tool with a simple Swing GUI front-end. Its release and development site are both found here via our download page.
- ESC/Java2 is also an Eclipse 3.4 plugin. Its homepage is currently hosted at Kansas State University.
Feedback
There are two mailing lists that focus on ESC/Java2:
- The JMLSpecs-ESCJava mailing list is the "users" mailing list where one can ask questions of experienced users and the developers of ESC/Java2. Subscribe to this list by registering at SourceForge.
- The ESCJava-Developers list is used by ESC/Java2 developers to discuss new features, bugs, designs, research, etc.