2001 | OriginalPaper | Buchkapitel
Houdini, an Annotation Assistant for ESC/Java
verfasst von : Cormac Flanagan, K. Rustan M. Leino
Erschienen in: FME 2001: Formal Methods for Increasing Software Productivity
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.