The Extended Static Checker for Java (ESC/Java) is a programming tool that statically detects software defects. ESC/Java works by translating each method into a verification condition, and then checking the validity of that verification condition. ESC/Java is a modular checker, and can check one method for errors without needing to analyze the entire program. This talk provides an overview of ESC/Java, and describes two technical advances necessary to make this approach practical.

First, current verification condition (VC) generation algorithms, such as weakest preconditions, yield a verification condition whose size may be exponential in the size of the code fragment being checked. ESC/Java includes a novel algorithm that generates polynomial-sized verification conditions. This algorithm has allowed us to check large and complex methods that would otherwise be impossible to check due to time and space constraints.

Second, since ESC/Java performs modular checking, it requires that each module be accompanied by annotations that specify the module. To reduce the cost of writing specifications, we have developed an annotation assistant for ESC/Java, called Houdini. Houdini infers suitable ESC/Java annotations by generating a large number of candidate annotations and using ESC/Java to verify or refute each of these annotations. Preliminary results suggest that Houdini significantly reduces the cost of using ESC/Java to check existing, unannotated programs.

Monday, April 2 at 4pm in DH 3092

A reception will be held BEFORE the talk at 3:30 in DH 3092.