Formal Verification of Code Conversion: A Comprehensive Survey
Amira T. Mahmoud,
Ahmad A. Mohammed,
Mahitap Ayman,
Walaa Medhat ,
Sahar Selim ,
Hala Zayed,
Ahmed H. Yousef,
Nahla Elaraby
Affiliations
Amira T. Mahmoud
Center for Informatics Science (CIS), School of Information Technology and Computer Science, Nile University, 26th of July Corridor, Sheikh Zayed City 12588, Egypt
Ahmad A. Mohammed
Center for Informatics Science (CIS), School of Information Technology and Computer Science, Nile University, 26th of July Corridor, Sheikh Zayed City 12588, Egypt
Mahitap Ayman
Center for Informatics Science (CIS), School of Information Technology and Computer Science, Nile University, 26th of July Corridor, Sheikh Zayed City 12588, Egypt
Walaa Medhat
Center for Informatics Science (CIS), School of Information Technology and Computer Science, Nile University, 26th of July Corridor, Sheikh Zayed City 12588, Egypt
Sahar Selim
Center for Informatics Science (CIS), School of Information Technology and Computer Science, Nile University, 26th of July Corridor, Sheikh Zayed City 12588, Egypt
Hala Zayed
Faculty of Computer and Artificial Intelligence, Department of Information Systems, Benha University, Banha 13511, Egypt
Ahmed H. Yousef
Faculty of Engineering, Egypt University of Informatics, Cairo 15702, Egypt
Nahla Elaraby
Institute of Computer Technology, Technical University of Vienna (TU Wien), 1040 Vienna, Austria
Code conversion, encompassing translation, optimization, and generation, is becoming increasingly critical in information systems and the software industry. Traditional validation methods, such as test cases and code coverage metrics, often fail to ensure the correctness, completeness, and equivalence of converted code to its original form. Formal verification emerges as a crucial methodology to address these limitations. Although numerous surveys have explored formal verification in various contexts, a significant research gap exists in pinpointing appropriate formal verification approaches to code conversion tasks. This paper provides a detailed survey of formal verification techniques applicable to code conversion. This survey identifies the strengths and limitations of contemporary adopted approaches while outlining a trajectory for future research, emphasizing the need for automated and scalable verification tools. The novel categorization of formal verification methods provided in this paper serves as a foundational guide for researchers seeking to enhance the reliability of code conversion processes.
