SRC Technical Note 2000-003
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.
Back to the SRC Technical Notes main page.
Download note as: