Houdini, an annotation assistant for ESC/Java. (English) Zbl 0977.68671

Flanagan, Cormac; Leino, K. Rustan M.

Oliveira, José Nuno (ed.) et al., FME 2001: Formal methods for increasing software productivity. International symposium of formal methods Europe, Berlin, Germany, March 12-16, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2021, 500-517 (2001).

Summary: 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.
For the entire collection see [Zbl 0977.68852].

MSC:

68U99	Computing methodologies and applications
68Q65	Abstract data types; algebraic specification

Software:

Houdini; Mercator