Verification of an Anti-unification Algorithm in PVS

M. Ayala-Rincón; Thaynara Arielly de Lima; Maria Júlia Dias Lima; Mariano Miguel Moscato; Teimuraz Kutsia

doi:10.1007/978-3-031-93706-4_4

Verification of an Anti-unification Algorithm in PVS

M. Ayala-Rincón^*
, Thaynara Arielly de Lima
, Maria Júlia Dias Lima
, Mariano Miguel Moscato
, Teimuraz Kutsia

^*Corresponding author for this work

Research Institute for Symbolic Computation

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Anti-unification is the problem of computing the commonalities between syntactic terms. Among its main applications, the detection of code regularities stands out since it is widely used in industrial settings as the foundation for technologies for the recognition of code-cloning, improvement of parallel compilation, and software error detection and correction. This paper discusses the verification of an anti-unification algorithm in the Prototype Verification System (PVS). The algorithm is based on inference rules that constructively compute the common structure between two terms, providing a substitution that expresses the least general generalizer between them as output. To the best of the authors’ knowledge, this is the first formalization of an anti-unification procedure containing proofs of relevant properties, such as termination and soundness.

Original language	English
Title of host publication	NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings
Editors	Aaron Dutle, Laura Humphrey, Laura Titolo
Place of Publication	Springer Verlag
Pages	54-71
Number of pages	18
Edition	1
DOIs	https://doi.org/10.1007/978-3-031-93706-4_4
Publication status	Published - 2025

Publication series

Name	Lecture Notes in Computer Science
Volume	15682 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

101013 Mathematical logic
101 Mathematics
101012 Combinatorics
101005 Computer algebra
101009 Geometry
101001 Algebra
101020 Technical mathematics

JKU Focus areas

Digital Transformation

Access to Document

10.1007/978-3-031-93706-4_4

Cite this

Ayala-Rincón, M., de Lima, T. A., Dias Lima, M. J., Moscato, M. M., & Kutsia, T. (2025). Verification of an Anti-unification Algorithm in PVS. In A. Dutle, L. Humphrey, & L. Titolo (Eds.), NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings (1 ed., pp. 54-71). (Lecture Notes in Computer Science; Vol. 15682 LNCS).. https://doi.org/10.1007/978-3-031-93706-4_4

@inproceedings{a35ac4e082cc4c0982193bedc876bde8,

title = "Verification of an Anti-unification Algorithm in PVS",

abstract = "Anti-unification is the problem of computing the commonalities between syntactic terms. Among its main applications, the detection of code regularities stands out since it is widely used in industrial settings as the foundation for technologies for the recognition of code-cloning, improvement of parallel compilation, and software error detection and correction. This paper discusses the verification of an anti-unification algorithm in the Prototype Verification System (PVS). The algorithm is based on inference rules that constructively compute the common structure between two terms, providing a substitution that expresses the least general generalizer between them as output. To the best of the authors{\textquoteright} knowledge, this is the first formalization of an anti-unification procedure containing proofs of relevant properties, such as termination and soundness.",

author = "M. Ayala-Rinc{\'o}n and \{de Lima\}, \{Thaynara Arielly\} and \{Dias Lima\}, \{Maria J{\'u}lia\} and Moscato, \{Mariano Miguel\} and Teimuraz Kutsia",

year = "2025",

doi = "10.1007/978-3-031-93706-4\_4",

language = "English",

isbn = " 978-3-031-93705-7",

series = "Lecture Notes in Computer Science",

pages = "54--71",

editor = "Aaron Dutle and Laura Humphrey and Laura Titolo",

booktitle = "NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings",

edition = "1",

}

Ayala-Rincón, M, de Lima, TA, Dias Lima, MJ, Moscato, MM & Kutsia, T 2025, Verification of an Anti-unification Algorithm in PVS. in A Dutle, L Humphrey & L Titolo (eds), NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 15682 LNCS, Springer Verlag, pp. 54-71. https://doi.org/10.1007/978-3-031-93706-4_4

Verification of an Anti-unification Algorithm in PVS. / Ayala-Rincón, M.; de Lima, Thaynara Arielly; Dias Lima, Maria Júlia et al.
NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings. ed. / Aaron Dutle; Laura Humphrey; Laura Titolo. 1. ed. Springer Verlag, 2025. p. 54-71 (Lecture Notes in Computer Science; Vol. 15682 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Verification of an Anti-unification Algorithm in PVS

AU - Ayala-Rincón, M.

AU - de Lima, Thaynara Arielly

AU - Dias Lima, Maria Júlia

AU - Moscato, Mariano Miguel

AU - Kutsia, Teimuraz

PY - 2025

Y1 - 2025

N2 - Anti-unification is the problem of computing the commonalities between syntactic terms. Among its main applications, the detection of code regularities stands out since it is widely used in industrial settings as the foundation for technologies for the recognition of code-cloning, improvement of parallel compilation, and software error detection and correction. This paper discusses the verification of an anti-unification algorithm in the Prototype Verification System (PVS). The algorithm is based on inference rules that constructively compute the common structure between two terms, providing a substitution that expresses the least general generalizer between them as output. To the best of the authors’ knowledge, this is the first formalization of an anti-unification procedure containing proofs of relevant properties, such as termination and soundness.

AB - Anti-unification is the problem of computing the commonalities between syntactic terms. Among its main applications, the detection of code regularities stands out since it is widely used in industrial settings as the foundation for technologies for the recognition of code-cloning, improvement of parallel compilation, and software error detection and correction. This paper discusses the verification of an anti-unification algorithm in the Prototype Verification System (PVS). The algorithm is based on inference rules that constructively compute the common structure between two terms, providing a substitution that expresses the least general generalizer between them as output. To the best of the authors’ knowledge, this is the first formalization of an anti-unification procedure containing proofs of relevant properties, such as termination and soundness.

UR - https://www.scopus.com/pages/publications/105008761802

U2 - 10.1007/978-3-031-93706-4_4

DO - 10.1007/978-3-031-93706-4_4

M3 - Conference proceedings

SN - 978-3-031-93705-7

T3 - Lecture Notes in Computer Science

SP - 54

EP - 71

BT - NASA Formal Methods - 17th International Symposium, NFM 2025, Proceedings

A2 - Dutle, Aaron

A2 - Humphrey, Laura

A2 - Titolo, Laura

CY - Springer Verlag

ER -

Verification of an Anti-unification Algorithm in PVS

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this