Portal de Periódicos da CAPES

Houdini, an Annotation Assistant for ESC/Java

2001; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45251-6_29

1611-3349

Cormac Flanagan, K. Rustan M. Leino,

Formal Methods in Verification

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 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.