Databases Reference
In-Depth Information
[generateSecret]
[doPhase]
0
[generateSecret]
2
1
[init]
[doPhase]
[generateSecret]
3
(a)
[init]
[doPhase]
[generateSecret]
0
1
2
3
(b)
FIGURE 6.14:
KeyAgreement
API with Past/Exterior merge and (a) Base
aliasing; and (b) APFocus aliasing.
finding existing code fragments that bring the program to a specified
desired state (a natural, more powerful, extension of [22]).
The quality of the mined specification should be evaluated with respect
to its particular usage. For example, a specification mined for the purpose
of program understanding should be human-readable, where a specification
mined for identifying deviant behaviors may ignore such a requirement.
Our experiments indicate that having both a precise-enough heap abstrac-
tion and a precise-enough history abstraction is required to be able to mine a
reasonable specification for either of the aforementioned usage scenarios.
Without such precise abstractions, the collected abstract histories might
deteriorate to a point in which no summarization algorithm will recover the
lost information. For example, the specification mined for the
Photo
API using
the Base heap abstraction has a single state. This means that the specification
does not contain any temporal information on the ordering of events (similarly
for
PrintWriter
under Base/Past/Total.)
6.7.3.1
Soundness
All of the results in Table 6.3 were obtained when our analysis was run
to completion, and are therefore guaranteed to be an over-approximation of
the behavior present in the analyzed code base. In contrast, it is also possible
to employ our analysis with a predetermined timeout (or with, e.g., a small
limited heap size). In such cases, the specification obtained using the analysis
will not over-approximate code base behavior, but may still help understand
some behaviors. For example, when running on TVLA, we mined a partial
but interesting description of the way
tvla.Engine
is used in the code base.
Search WWH ::
Custom Search