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
3:30pm
Wean 8220