Anti-unification Algorithms and Their Applications in Program Analysis

A term t is called a template of terms t1 and t2 iff t1 = t1 and t2 = t2, for some substitutions 1 and 2. A template t of t1 and t2 is called the most specific iff for any template t of t1 and t2 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 labeled directed acyclic graphs and estimate the complexity of the anti-unification problem. We also describe techniques for invariant generation and software clone detection, which are based on the concepts of the most specific templates and antiu...

• Type: Conference
• Year: 2009
• Where: ERSHOV
• Authors: Peter E. Bulychev, Egor V. Kostylev, Vladimir A. Zakharov
• Keywords: Anti-unification Problem, ERSHOV 2009, Specific Template, Theoretical Computer Science, Well-known Unification Problem