Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 296

is also statistical. Furthermore, they use a set of specific names to reduce the
number of candidate events [24]. In order to infer a property, Engler's tech-
nique requires that an event (e.g., a function foo ) occurs frequently enough
in the code base (e.g., foo is called at many different places). In contrast, our
dynamic technique can still infer a property as long as an event occurs fre-
quently enough in the trace. The limitation of Engler's work is that it often
produces too many false positives. To lower the rate of false positives, Weimer
et al. improved Engler's work by developing an approach that examines a pro-
gram's exception handling routines [79]. The intuition is that programs often
make mistakes on exceptional paths, even when they are mostly correct on
the normal paths. On one hand, Weimer's approach mainly focuses on local
properties, while our technique can identify relationships among events that
are far removed from each other in program text. On the other hand, Weimer's
work and our work complement each other because it is usually very hard to
generate test inputs for exception handling routines.
Houdini is an annotation inference tool for ESC [28, 29]. The annota-
tions are in the standard Hoare-style logic that includes pre-condition, post-
condition, and invariants [41]. Houdini first generates a set of candidate anno-
tations and then feeds these candidates to ESC. ESC either proves or refutes
a property. The main problem of Houdini is that it does not scale well because
the underlying ESC is slow.
Other static inference techniques focus on certain program features and are
very effective. LockSmith is a tool for automatically inferring locking discipline
annotations that are later used to check for deadlocks and race conditions [66].
SALInfer is a tool for inferring annotations for function arguments that are
related to buffer usages [37]. SALInfer has been successfully used to help
annotate the whole Windows code-base. Both LockSmith and SALInfer use
dataflow analysis. Compared to LockSmith, Perracotta infers a similar type of
property using a regular expression inference from execution traces. Compared
to SALInfer, our work focuses on a different class of properties that SALInfer
does not infer. Furthermore, our underlying technique is based on regular
expression matching instead of dataflow analysis.

8.5.2.2 Arbitrary Model Inference

Arbitrary model inference techniques try to discover a model that fits the
target program or its execution traces. Most of the related work in this cate-
gory analyzes program execution traces [3,13,69,81]. Other artifacts analyzed
include revision history [58] and source code [30].
Ammons et al. used an off-the-shelf probabilistic finite state automaton
learner to mine temporal and data-dependence specifications for APIs or ab-
stract data structures from dynamic traces [3, 4]. In addition to handling of
traces containing bugs (i.e., imperfect traces as defined in our work), their
approach required non-trivial human guidance. In contrast, our techniques
can automatically tolerate imperfect traces without guidance. Their machine