ESC/Java2 (Extended Static Checker) ist ein erweitertes statisches Prüfprogramm für Java. Es erkennt häufige Programmierfehler automatisch, statisch und modular. Es wird auf Java-Programme angewandt, die optionale Anmerkungen in JML haben können. (non)