Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Anti-unification Algorithms and Their Applications in Program Analysis
verfasst von : Peter E. Bulychev, Egor V. Kostylev, Vladimir A. Zakharov
Erschienen in: Perspectives of Systems Informatics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
A term
t
is called a
template
of terms
t
1
and
t
2
iff
t
1
=
tη
1
and
t
2
=
tη
2
, for some substitutions
η
1
and
η
2
. A template
t
of
t
1
and
t
2
is called
the most specific
iff for any template
t
′ of
t
1
and
t
2
there exists a substitution
ξ
such that
t
=
t
′
ξ
. The anti-unification problem is that of computing the most specific template of two given terms. This problem is dual to the well-known unification problem, which is the computing of the most general instance of terms. Unification is used extensively in automatic theorem proving and logic programming. We believe that anti-unification algorithms may have wide applications in program analysis. In this paper we present an efficient algorithm for computing the most specific templates of terms represented by labelled directed acyclic graphs and estimate the complexity of the anti-unification problem. We also describe techniques for invariant generation and software clone detection based on the concepts of the most specific templates and anti-unification.