Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 348

20

total number of procedures
dynamic inference
non−profile based inference
static profile based inference

15

10

5

0

F1 F2 F3

Number of call−sites

FIGURE 9.21: Correctness of different inference schemes. (With kind per-
mission from Springer Science + Business Media: Protocol Inference Using
Static Path Proles, SAS, 2008, pp. 78{92, M. Ramanthan et al., Figure 8.)

importantly, when it becomes dicult to reason with symbolic constraints,
concrete values from the program execution replace symbols to ensure progress
of the test input generation process. We refer the reader to [39] for a more
detailed description.
We track the predicates along different execution paths of the program
and for each call to a procedure, group the set of predicates that precede it
from the start of the execution. Thus, across multiple executions, we would
generate many such groups of predicates. To generate the precondition for the
procedure, we apply frequent item-set mining [11]. The frequently occurring
predicates across all the groups form the precondition.
We performed our comparison on buddy , an open source package that im-
plements operations over Binary Decision Diagrams (BDD). We rancutefor
a bounded number of iterations (1000), which took approximately 30 minutes,
and in that process collected specifications for 24 procedures. Of these 24 pro-
cedures, only 2 procedures (F1) had more than 10 call-sites, 3 procedures (F2)
had call-sites between 5 and 10, and the remaining 19 procedures (F3) had
less than 5 call-sites. Using existing documentation, and manual inspection,
we computed a reference specification for each of these procedures.
Figure 9.21 presents the results associated with our qualitative analysis.
We applied three different schemes: (1) dynamic inference, (2) non-profile
based inference, and (3) path-profile based inference on this benchmark. For
the set of two procedures in F1, all techniques provide similar precision
and were able to detect preconditions correctly for one procedure. Under-
approximation confounds the precision of dynamic inference for the set of
three procedures in F2. The analysis for the procedures in F3 is more in-
teresting. Because of the lack of frequency of call-sites for the procedures in