RISC Forum
Prof. Dr. Mauricio-Ayala-Rincon: On the Computational Verification of Anti-unification
Abstract: Anti-unification, or generalization, is the algebraic problem of determining the commonalities between two expressions. The problem is crucial in computation, particularly in the automation of equational reasoning, with applications ranging from detecting regularities in code to detecting commonalities in data. Anti-unification algorithms are used in industrial tools devoted, for instance, to efficient parallel computation, plagiarism detection, and automatic code correction. This talk will present a functional algorithm for anti-unification and discuss a mechanical verification of the algorithm formalized in the Prototype Verification System PVS.