Abstract

The Extended Static Checker for Java (ESC/Java) is a programming tool for finding, at compile-time, common programming errors that usually are not found until run-time, and sometimes not even then. The tool is powered by program verification technology, but feels to a user more like a type checker. To use it, a programmer adds simple annotations to the program.

In this talk, I will give an overview of the system, give a short demo, discuss our experience in using the checker on real Java programs, and touch on some future directions.