Download Houdini, an Annotation Assistant for ESC/Java

Abstract
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 accompanied by annotations that specify the module. To help reduce the cost of
writing specifications, this paper presents Houdini, an annotation assistant 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.
A version of this paper will appear in the proceedings of Formal Methods Europe
(FME’01), 2001.