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 accom-panied by annotations that specify the module. To help reduce the cost of writing Specification, 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. © Springer-Verlag Berlin Heidelberg 2001.