Abstract
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.
The research is supported by RFBR grants 09-01-00277 and 09-01-00632.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 447–533 (2001)
Baxter, I., Yahin, A., Moura, L.M., Sant’Anna, M., Bier, L.: Clone Detection Using Abstract Syntax Trees. In: Proc. of the 14th IEEE International Conference on Software Maintenance, pp. 368–377 (1998)
Bille, P.: A survey on tree distance and related problems. Theoretical Computer Science 337(1-3), 217–239 (2005)
Bulychev, P.: Duplicate code detection using Clone Digger. PythonMagazine 9, 18–24 (2008)
Bulychev, P., Minea, M.: An evaluation of duplicate code detection using anti-unification. In: Proc. of the 3rd Int. Workshop on Software Clones, pp. 22–27 (2009)
Eder, E.: Properties of substitutions and unifications. Journal of Symbolic Computations 1, 31–46 (1985)
Evans, W., Fraser, C., Ma, F.: Clone detection via structural abstraction. In: Proc. of 14th Working Conference on Reverse Engineering, pp. 150–159 (2007)
Kovac, L.I., Jebelean, T.: An algorithm for automated generation of invariants for loops with conditionals. In: Proc. of the 7th Int. Symp. on Symbolic and Numeric Algorithms for Scientific Computing, pp. 245–250 (2005)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis, 446 p. Springer, Heidelberg (1999)
Oancea, C.E., So, C., Watt, S.M.: Generalization in Maple. In: Maple Conference, pp. 277–382 (2005)
Palamidessi, C.: Algebraic properties of idempotent substitutions. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 386–399. Springer, Heidelberg (1990)
Plotkin, G.D.: A note on inductive generalization. Machine Intelligence 5(1), 153–163 (1970)
Reynolds, J.C.: Transformational systems and the algebraic structure of atomic formulas. Machine Intelligence 5(1), 135–151 (1970)
Roy, C.K., Cordy, J.R.: A survey on software clone detection research. Technical Report N 2007-541, School of Computing Queen’s University at Kingston Ontario, Canada
Sorensen, M.H.: Gluck. R. An algorithm of generalization in positive supercompilation. In: Proc. of the 1995 Int. Symposium on Logic Programming, pp. 465–479. MIT Press, Cambridge (1995)
Tiwari, A., Rueb, H., Saidi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)
Watt, S.M.: Algebraic generalization. ACM SIGSAM Bulletin 39(3), 93–94 (2005)
Wettel, R., Marinescu, R.: Archeology of Code Duplication: Recovering Duplication Chains From Small Duplication Fragments. In: Proc. of the 7th Int. Symb. on Symbolic and Numeric Algorithms for Scientific Computing, pp. 63–70 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bulychev, P.E., Kostylev, E.V., Zakharov, V.A. (2010). Anti-unification Algorithms and Their Applications in Program Analysis. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-11486-1_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11485-4
Online ISBN: 978-3-642-11486-1
eBook Packages: Computer ScienceComputer Science (R0)