ESC/Java

This is an old revision of this page, as edited by Redjamjar (talk | contribs) at 20:24, 6 July 2010 (Corrected missing RefList). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs by static analysis of the program text[1]. Recent versions of ESC/Java are based around the Java Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or pragmas.

ESC/Java was originally developed at the Compaq Systems Research Center (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the source code for ESC/Java and related tools.

The University of Nijmegen's Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the JML specification language through 2004. Since 2004, ESC/Java2 development has been managed by the KindSoftware Research Group at University College Dublin. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple theorem provers and integration with Eclipse.

References

  1. ^ C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata. "Extended static checking for Java". In Proceedings of the Conference on Programming Language Design and Implementation, pages 234--245, 2002. doi: http://doi.acm.org/10.1145/512529.512558