Databases Reference
In-Depth Information
to detect whether and how a program fits in a specific pattern, whereas an
arbitrary model inference technique tries to create the best model that fits
the target program or its execution traces.
We can further classify techniques in each of the two main categories into
two subcategories: machine learning-based techniques that use statistical ma-
chine learning to infer patterns [3, 13, 24, 25, 38, 58, 69, 79, 81], and dataflow
analysis-based techniques that infer properties by either symbolically execut-
ing a program [30,37,66] or using a verification tool as an oracle [28]. Following
subsections compare our work with the work in each category.
8.5.2.1
Template-Based Inference
Template-based inference techniques have a set of pre-defined templates
that can capture pre-condition, post-condition, and invariants [26,28,38], tem-
poral constraints [24, 79], or very specific program features such as locks [66]
or buers [37].
Daikon is a tool that automatically infers likely program invariants from a
program's execution traces [25, 26, 65]. The technique uses a set of pre-dened
invariant patterns that are matched against the values observed in the traces;
invariants that are violated are dropped. Invariants that survive are ranked
in order of confidence. Only invariants that are above a specified confidence
threshold are reported. The original Daikon inference algorithm is limited
by its scalability because the algorithm is cubic in the number of variables
monitored [26]. Several new optimizations recently developed by Perkins and
Ernst greatly improve Daikon's performance, but performance remains an
impediment to applying Daikon to large-scale programs [65]. Our work is
distinct from Daikon in that our approach infers specifications of the temporal
behaviors of a system, which Daikon does not infer. Our technique also scales
much better to large-scale real systems such as Windows. In addition, Daikon
requires 100% satisfaction of templates and therefore is less robust to imperfect
traces than our approximate inference algorithm.
Diduce is a run-time anomaly detection tool that is based on invariant in-
ference [38]. Diduce infers data invariants as a program executes and generates
alarms whenever the execution violates the current invariants. The invariants
Diduce infers are bit field patterns (e.g., the last bit of a byte at certain ad-
dress is always 0) and therefore are useful for detecting memory usage errors
at runtime. Our work is different from Diduce in that our work focuses on
API level invariants. In addition, the properties Perracotta infers can be used
for several other purposes other than run-time monitoring.
Engler et al. proposed a method for extracting properties by statically ex-
amining source code based on a set of pre-defined templates [24]. Like our
approach, their technique scales well by targeting simple property templates.
Our chaining method can build more complex properties that their technique
does not infer. To deal with the imprecision of static analysis, they use statis-
tics to prioritize their results. Similarly, our approximate inference algorithm
Search WWH ::
Custom Search