Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
ExplainHoudini: Making Houdini inference transparent

Shuvendu K. Lahiri and Julien Vanegue

Abstract

Houdini is a simple yet scalable technique for annotation inference for modular contract checking. The input to Houdini is a set of candidate annotations, and the output is a consistent subset of these candidates. Since this technique is most useful as an annotation assistant for user-guided refinement of annotations, understanding the reason for the removal of annotations is crucial for a user to refine the set of annotations, and classify false errors easily. This is especially true for applying Houdini to large legacy modules with thousands of procedures and deep call chains. In this work we present a method it ExplainHoudini that explains the reason why a given candidate was removed, purely in terms of the existing candidates. We have implemented this algorithm and provide preliminary experience of applying it on large modules.

Details

Publication typeTechReport
NumberMSR-TR-2010-118
PublisherSpringer Verlag
> Publications > ExplainHoudini: Making Houdini inference transparent