ESCSubsystemsExplanation

ESC/Java2 has been under development for over a decade. The original ESC/Java was developed by a team at Digital Equipment Corporation's Systems Research Center in the mid-1990s. After that team disbanded and DEC-SRC was shut down (after Compaq bought Digital and then Hewlett-Packard bought Compaq), Hewlett-Packard released the source code of ESC/java for research and educational purposes.

At that time, a team at Radboud University Nijmegen, led by Joe Kiniry, restarted research and development on Extended Static Checking for Java, and have since then released over fifteen versions of ESC/Java2. ESC/Java2 shares only a few subsystems with the original ESC/Java.

This page summarizes the core subsystems of the current release of ESC/Java2 (2.0b4) included with the Mobius PVE that remain from the original ESC/Java. All other extensions to ESC/Java2 that have taken place over the past five years are described in other sections, as they have all been incorporated into the Mobius PVE itself. These extensions include the new VC ASTs, the Automated Prover API, the the new Fx7 and Z3 backends, universes typechecking, and support for higher-order extended static checking, which is not discussed in this page.

Version: 2 Time: Tue Apr 1 18:02:15 2008 Author: dcochran (dcochran) IP: 193.1.132.32