paper

ESC/Java User Manual

  • Authors:
Read the paper

đź“ś Abstract

ESC/Java is a program checker that automatically, or nearly automatically, detects common programming errors. This manual describes ESC/Java, emphasizes how to use it effectively, and serves as a source of reference information.

✨ Summary

The paper “ESC/Java User Manual” published in 2001 presents ESC/Java, a tool designed to perform static checking of Java programs to detect common programming errors. The tool leverages specifications attached to Java programs and provides warnings for potential errors at compile-time. This approach aids developers in verifying code behavior against specified assertions, potentially reducing runtime errors and improving code reliability significantly.

ESC/Java serves as a precursor to advancements in software verification and static analysis tools, influencing many subsequent developments in the field of formal methods and program verification. Despite its age, it is still referenced in literature concerning program verification and static analysis. For example, the work on ESC/Java has been cited by Leino et al. in academic resources focusing on software correctness and analytical methods.

References: 1. Andrea Arcuri, Lionel C. Briand, “A Practical Guide for Using Statistical Tests to Assess Randomized Algorithms in Software Engineering”, Proceedings of the 33rd International Conference on Software Engineering, 2011. 2. K. Rustan M. Leino, “Efficient weakest preconditions”, Information Processing Letters, 2005, Elsevier.