Databases Reference
In-Depth Information
Ernst et al. studied using the invariants inferred by Daikon to aid program-
mers in modifying programs [26]. In their experiments, programmers were
supplied with the inferred invariants, as they added a new feature to an exist-
ing program. The programmers found the inferred invariants useful. Our work
on using inferred invariants in dierencing programs was inspired by Ernst's
work. Compared to Ernst's work, our work focused more on automatically
detecting the semantic difference of multiple versions of a program, whereas
Ernst's work aimed to evaluate whether the inferred specication could be
useful for programmers.
Naturally, inferred specifications can be used to help programmers gain
more insights into the target program. Cook et al. developed a technique for
inferring thread interaction models from execution traces [13]. Their technique
used a statistical approach. Mandelin et al. developed a technique for discov-
ering the sequence of APIs that were needed to accomplish some tasks [59].
They called their tool specification prospector and the inferred API sequence
jungloid. Our work on inferring
Alternating Chains
bore a similar motivation as
Mandelin's work.
Another representative use of inferred specifications is in guiding theorem
prover to verify distributed programs [82].
Liblit et al. showed the inferred specifications can be used to debug a pro-
gram [56]. Their work monitored a set of program predicates and compared
the observed properties of a successful execution against the ones of a failed
execution. Their technique used a statistical approach to eliminate irrelevant
predicates and rank inferred predicates. One big advantage of this work com-
pared to previous work on bug localization is that it can effectively handle
programs that have more than one bug. We also plan to investigate whether
the temporal specifications inferred by Perracotta can be useful in debugging.
Much work has been on using inferred specifications to detect bugs, Dem-
sky et al. showed that the inferred specification can also be used to let a
program continue its execution in face of data structure corruption [20]. Their
technique used Daikon to infer invariants for data structures and automati-
cally detected and restored corrupted data structures to behave normally with
regard to the invariants.
8.6 Conclusion
Software specifications are the foundation of many software development
activities including maintenance, testing, and verification. We have presented
Perracotta, a tool that automatically infers temporal specifications of pro-
grams by analyzing execution traces. Perfect, fully automatic specification
inference for industrial programs remains an elusive goal, well beyond the
Search WWH ::
Custom Search