Extended static checking for Java

certain errors that are normally not detected until run time, and sometimes
not even then. For example, array bounds errors, null dereferences, and
race conditions and deadlocks in multi-threaded programs. The system requires
the programmer to annotate method declarations with simple preconditions
and postconditions. These annotations are much less onerous than the
annotations that would be required for a full program correctness proof.
Once the program is annotated, the checking is totally automatic. The
checker reports errors by line number. The system handles essentially
all features of the Java 1.0 language, including concurrency. Many parts
of the standard Java libraries and of the checker itself have been checked
with the system. I'll also give a demonstration of the system, weather
permitting.