HoudiniExplanation

Like the Race Condition Checker (RCC), Houdini was also originally developed by researchers at the Digital Systems Research Lab (DEC-SRC) in the late 1990s (FL00). Its source code was released to the general public along with the source for Simplify, Javafe, ESC/Java2, and RCC.

Houdini automatically generates specifications written in JML for a Java module by statically analyzing the structure of program code. It has a number of built-in heuristics and performs some lightweight syntactic and semantic reasoning about method bodies to "guess" potential method preconditions, for example. These guesses are then fed to ESC/Java2 to see whether or not they are valid. If a specification seems to be valid (recall that ESC/Java2 is neither sound nor complete), then the specification is retained, otherwise it is discarded.

Houdini generates reports of its behavior in HTML. Houdini is also capable of taking a snapshot of its state for increasing the reliability of long runs (as running Houdini on a large code base can take hours, or even days). Finally, Houdini can run in a client-server mode, utilizing a (potentially larger, and more powerful) remote compute server.

Version: 1 Time: Fri Mar 28 13:31:30 2008 Author: dcochran (dcochran) IP: 193.1.132.32