Mark Lillibridge

Extended Static Checking for Java

This talk describes an experimental automatic checker that catches many common programming errors, including array bounds errors, null dereference errors, and synchronization errors in multi-threaded programs. The checking is performed at compile-time. The checker uses an automatic theorem-prover to reason about the semantics of conditional statements, loops, procedure and method calls, and exceptions. The checker has been implemented in and for Java. The checker has been run on classes comprising more than thirty thousand lines of code. A demonstration will be given.
February 3, 1999
Wean 8220