Databases Reference
In-Depth Information
procedure to learn a permissive interface of a given component. Nandi et
al. [24] use static mining to learn a permissive first-order specification involving
objects, their relationships, and their internal states.
Client-Side Static Analysis. A few papers have applied static analysis to
client-side specification mining.
Engler et al. [9] use various static analyses to identify common program
behaviors, and consider deviations from these behaviors as bugs. Their ap-
proach automatically establishes certain invariants as likely beliefs, and the
tool searches for bugs by finding code sequences that violate these invariants.
The tool searches for invariants based on a set of standard templates, and
filters potential specifications with a statistical measure (z-ranking). Their
approach has been highly effective in finding bugs in system code.
Weimer and Necula [30] use a simple, lightweight static analysis to infer
simple specifications from a given codebase. Their insight is to use exceptional
program paths as negative examples for correct API usage. We believe that our
approach could also benefit from using exceptional paths as negative examples.
Weimer and Necula learn specications that consist of pairs of events ha;bi,
where a and b are method calls, and do not consider larger automata. They
rely on type-based alias analysis, and so their techniques should be much less
precise than ours. On the other hand, their paper demonstrates that even
simple techniques can be surprisingly effective in finding bugs.
Mandelin et al. [22] use static analysis to infer a sequence of code (jungloid )
that shows the programmer how to obtain a desired target type from a given
source type (a jungloid query ). This code-sequence is only checked for type-
safety and does not address the finer notion of typestate. In contrast, our
approach focuses on mining temporal specifications.
Wasylkowski et al. [29] use an intraprocedural static analysis to automati-
cally mine object usage patterns and identify usage anomalies. Their approach
is based on identifying usage patterns. In contrast, our approach mines tem-
poral specifications that over-approximate the usage scenarios in a code-base.
Other Static Analyses. [17] presents a model-extraction technique and ex-
tracts both the object relationships and a model of their interactions. This
approach requires user annotation that associates a \token" with every object
of interest and uses static analysis to infer the relationships and interactions
between tokens. In contrast, our approach currently focuses only on typestate
specifications, but is fully automatic.
Lie et al. [18] present an approach to extract state transition models using
an extensible compiler, xg++. In this work, the user specifies patterns corre-
sponding to state variables and operations relevant to a particular protocol.
Based on this specification, the compiler slices the program to elide irrelevant
statements, and then performs a simple user-guided translation to output the
model in a desired form, suitable for input to a model-checker. This work
targets low-level cache coherency protocols implemented in C.
Search WWH ::
Custom Search