On the application of substitution algebra to program unification
Many problems in software engineering such as program refactoring, deobfuscation, vulnerability detection, require an efficient toolset for detecting pieces of code that have similar behavior. Current state of art in software clone detection makes it possible to find out only those pieces of code wh...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/1035 |
| _version_ | 1818807342370652160 |
|---|---|
| author | V. A. Zakharov T. A. Novikova |
| author_facet | V. A. Zakharov T. A. Novikova |
| author_sort | V. A. Zakharov |
| collection | DOAJ |
| description | Many problems in software engineering such as program refactoring, deobfuscation, vulnerability detection, require an efficient toolset for detecting pieces of code that have similar behavior. Current state of art in software clone detection makes it possible to find out only those pieces of code which have the same syntactic structure since. A more profound analysis of functional properties of programs encounters with undecidability of equivalence checking problem for Turing-complete models of computation. To overcome this principal deficiency of modern clone detection techniques we suggest to use equivalence relations on programs that are more strong than functional equivalence. One of such equivalences is a so called logic&term program equivalence introduced by V.E. Itkin in 1972 г. In this paper we build a new algorithm for checking logic&term equivalence of programs. This algorithm is based on the operations for computing the least upper bound and the greatest upper bound in the lattice of finite substitutions. Using this algorithm we also develop a procedure for solving the unification problem for sequential programs, i.e. the problem of computing the most general common instance (specialization) of a given pair of programs (pieces of code). |
| first_indexed | 2024-12-18T19:24:08Z |
| format | Article |
| id | doaj.art-335d9e833ae9499ab0a0edd620496032 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-18T19:24:08Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-335d9e833ae9499ab0a0edd6204960322022-12-21T20:55:54ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-012101035On the application of substitution algebra to program unificationV. A. Zakharov0T. A. Novikova1ИСП РАНф-т ВМК МГУ им. М.В. ЛомоносоваMany problems in software engineering such as program refactoring, deobfuscation, vulnerability detection, require an efficient toolset for detecting pieces of code that have similar behavior. Current state of art in software clone detection makes it possible to find out only those pieces of code which have the same syntactic structure since. A more profound analysis of functional properties of programs encounters with undecidability of equivalence checking problem for Turing-complete models of computation. To overcome this principal deficiency of modern clone detection techniques we suggest to use equivalence relations on programs that are more strong than functional equivalence. One of such equivalences is a so called logic&term program equivalence introduced by V.E. Itkin in 1972 г. In this paper we build a new algorithm for checking logic&term equivalence of programs. This algorithm is based on the operations for computing the least upper bound and the greatest upper bound in the lattice of finite substitutions. Using this algorithm we also develop a procedure for solving the unification problem for sequential programs, i.e. the problem of computing the most general common instance (specialization) of a given pair of programs (pieces of code).https://ispranproceedings.elpub.ru/jour/article/view/1035программаобнаружение клоновэквивалентностьподстановкаунификацияантиунификация |
| spellingShingle | V. A. Zakharov T. A. Novikova On the application of substitution algebra to program unification Труды Института системного программирования РАН программа обнаружение клонов эквивалентность подстановка унификация антиунификация |
| title | On the application of substitution algebra to program unification |
| title_full | On the application of substitution algebra to program unification |
| title_fullStr | On the application of substitution algebra to program unification |
| title_full_unstemmed | On the application of substitution algebra to program unification |
| title_short | On the application of substitution algebra to program unification |
| title_sort | on the application of substitution algebra to program unification |
| topic | программа обнаружение клонов эквивалентность подстановка унификация антиунификация |
| url | https://ispranproceedings.elpub.ru/jour/article/view/1035 |
| work_keys_str_mv | AT vazakharov ontheapplicationofsubstitutionalgebratoprogramunification AT tanovikova ontheapplicationofsubstitutionalgebratoprogramunification |