Anti-unification: Introduction, Applications, and Recent Results

Abstrakt

Anti-unification is a method for symbolically generalizing formal expression. It was introduced independently by Plotkin and Reynolds as an operation for inductive inferencing. Though conceptually simple, it is an effective tool for abstraction and templating. Since the seminal work, the number of applications has grown tremendously with uses in program analysis, program repair, library compression, automated reasoning, and beyond. With the growth of applications, there has been an effort to strengthen the theoretical foundations of the subject. In this talk, we introduce anti-unification, overview the existing applications, and discuss recent theoretical results concerning equational and high-order anti-unification.