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.

Cross-platform mobile application development is emerging widely in the mobile applications industry. Cross-platform Frameworks (CPFs) like React Native, Flutter, and Xamarin are used by many developing companies. The technology these frameworks use faces performance and resource use efficiency limitations compared to native applications. The native applications are written in the native languages of the platforms. Trans-complier-based conversion between native languages of different platforms of mobile applications has been addressed in recent research. However, the problem statement needed to be mathematically represented. The solution depended on hard coding and needed more generalization. In addition, it might not be a practical solution for companies that are using and already have built applications using CPFs. Therefore, in this paper, we present an enhanced-trans-compiler-based converter to convert applications made by CPFs to native applications. We implemented the architecture to convert React Native and Xamarin applications. The React Native to Native tool converted thirteen applications to native Android and iOS applications, with accuracies ranging from 40% for large applications to 100% for simple applications. The maximum conversion time was seven minutes for converting 40% of an 8K LOC application. In addition, since Large Language Models (LLMs) are the trendiest technology in our era, we compared our proposed solution output with LLMs. We concluded its superiority compared to the status of LLMs. Performance evaluation is also done to compare the React Native applications against native applications generated by the trans-compiler tool. The assessment showed that the native applications perform better than React Native regarding runtime memory consumption, storage, and speed. The Xamarin to Native tool was also tested to show the genericness of the architecture and how it can be extended to convert from any CPF to Native applications.

Code-to-code translation, a critical domain in software engineering, increasingly utilizes trans-compilers to translate between high-level languages. Traditionally, the fidelity of such translations has been evaluated using the BLEU score, which predominantly measures token similarity between the generated output and the ground truth. However, this metric falls short of assessing the methodologies underlying the translation processes and only evaluates the translations that are tested. To bridge this gap, this paper introduces an innovative architecture, “TC-Verifier”, to formally employ the Uppaal Model-checker to verify trans-compiler-based code translators. We applied the proposed architecture to a trans-compiler translating between Swift and Java, providing insights into the verified and unverified aspects of the translation process. Our findings illuminate the strengths and limitations of using Model-checking for formal verification in code translation. Notably, the examined trans-compiler reached a verification success rate of 50.74% for the grammar rules and productions modeled. This study underscores the gaps in trans-compiler-based translations and suggests that these gaps could potentially be addressed by integrating Large Language Models (LLMs) in future work.

Recent advances in Large Language Models (LLMs) have led to notable progress in automated code generation and translation tasks, yet concerns about trustworthiness and semantic reliability remain a challenge. Previous approaches often rely on fine-tuning with large amounts of parallel training data, which is impractical for low-resource languages where data scarcity amplifies error rates and undermines user confidence. In this paper, we present a hybrid approach, TC-assisted prompting, that combines transcompiler-based translators and LLMs to enhance code translation and increase trust in their outputs. The approach integrates transcompiler-based translations, which are verifiable but incomplete, into the prompts given to the LLMs, thereby improving code translation without requiring additional resource-intensive fine-tuning of pretrained models. To evaluate this method, we construct TGAlpaca, a new dataset comprising Java, JavaScript, and Swift snippets curated from programming tutorials and the HuggingFace Alpaca repository. Two instruction-tuned, code-specific LLMs (Codestral 25B and Qwencoder 32B), as well as the general-purpose GPT-4o-mini, are benchmarked under baseline and transcompiler-assisted (TC-assisted) prompting conditions. On TGAlpaca, our evaluation shows consistent improvements, from as little as 2% in Java→Swift to as high as 40% in JavaScript→Java, illustrating the potential of our approach. We further assess the methodology on XLCoST dataset using Codestral 25B model, its fine-tuned version, and its TC-assisted version. We observe that TC-assisted prompting can increase translation fidelity, reduce dependence on costly fine-tuning, and strengthen trust in LLM-assisted software engineering workflows.

Nowadays Mobile Applications are a necessity as everyone is depending on them in their everyday tasks. We use them for communication, entertainment, and utilities. Every day new devices are introduced to the market. The diversity in these devices resulted in many platforms like Android and iOS. These different mobile platforms used by different companies and manufacturers made it challenging for mobile developersto build an application or a system that can be deployed on different platforms. Developers will be required to go through multiple development cycles to develop the application for each of the targeted platforms. To solve these issues, cross-platform frameworks emerged as a solution that would help the developers to write one codebase and deploy it on multiple platforms at the same time. Even though cross-platform frameworks reduced the time and cost needed to develop an application, but they did not provide the native feel and performance of the native applications. It was also challenging for developers to integrate cross-platform applications with a pre-existing system and to maintain the system. Some approaches were introduced to solve these issues by allowing the developer to write one codebase and generate the native code for each platform. One of the recently presented approaches is the trans-compilation approach that depends on the parser code to recognize the source code and generate the corresponding code for it in the target language. Even though the trans-compiler-based approaches were effective in providing an application that combines the advantages of the cross-platform and native development, it faced some problems in dealing with statements that is not expressed in the language's grammar rules, eternal APIs, and APIs that require code definition, like Firebase. In this paper, our aim is to provide a solution that can be integrated with the trans-compilation approach to solve the previously mentioned issues to enhance the conversion success rate by recognizing statements and predict the corresponding ones