"Houdini, an Annotation Assistant for ESC/Java"
Cormac Flanagan and K. Rustan M. Leino
Note #2000-003, December 31, 2000. 


A static program checker that performs modular checking can check

one program module for errors without needing to analyze the entire

program. Modular checking requires that each module be accompa-nied

by annotations that specify the module. To help reduce the cost of

writing specifications, this paper presents Houdini, an annotation as-sistant

for the modular checker ESC/Java. To infer suitable ESC/Java

annotations for a given program, Houdini generates a large number of

candidate annotations and uses ESC/Java to verify or refute each of

these annotations. The paper describes the design, implementation,

and preliminary evaluation of Houdini.