MARC details
| 000 -LEADER |
|---|
| fixed length control field |
14786nam a22002657a 4500 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
201210b2025 a|||f bm|| 00| 0 eng d |
| 024 7# - Author Identifier |
|---|
| Standard number or code |
0000-0002-1702-6544 |
| Source of number or code |
ORCID |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
EG-CaNU |
| Transcribing agency |
EG-CaNU |
| 041 0# - Language Code |
|---|
| Language code of text |
eng |
| Language code of abstract |
eng |
| -- |
ara |
| 082 ## - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
627 |
| 100 0# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Amira Tarek Mahmoud Ibrahim |
| 245 1# - TITLE STATEMENT |
|---|
| Title |
Semi formally verified enhanced code translators of mobile applications programming languages |
| Statement of responsibility, etc. |
/Amira Tarek Mahmoud Ibrahim |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. |
|---|
| Date of publication, distribution, etc. |
2025 |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
152 p. |
| Other physical details |
ill. |
| Dimensions |
21 cm. |
| 500 ## - GENERAL NOTE |
|---|
| Materials specified |
Supervisor: <br/>Dr Walaa Medhat<br/>Prof Ahmed Hasan, Prof Hala Zayed, Dr Nahla Elaraby<br/> |
| 502 ## - Dissertation Note |
|---|
| Dissertation type |
Thesis (PH.D.)—Nile University, Egypt, 2025 . |
| 504 ## - Bibliography |
|---|
| Bibliography |
"Includes bibliographical references" |
| 505 0# - Contents |
|---|
| Formatted contents note |
Contents:<br/>Contents<br/>Page<br/>Copyright . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . III<br/>Dedication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . IV<br/>Acknowledgment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . V<br/>Declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . VI<br/>Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . VII<br/>List of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . XII<br/>List of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . XIV<br/>List of Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . XVI<br/>List of Abbreviations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . XVII<br/>1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1<br/>1.1 Dissertation Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3<br/>2. Mobile Applications Development in Industry . . . . . . . . . . . . . . . . . . . . . . . . 5<br/>2.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5<br/>2.2 Literature Review: Mobile Applications Development Industry-Related studies . . . 6<br/>2.3 Questionnaire Design and Methodology . . . . . . . . . . . . . . . . . . . . . . . . 7<br/>2.3.1 Questionnaire Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7<br/>2.3.2 Technical Question Flow and Content . . . . . . . . . . . . . . . . . . . . . 9<br/>2.3.3 Pilot Testing and Questionnaire Distribution Strategy . . . . . . . . . . . . 10<br/>2.3.4 Analysis Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10<br/>2.4 Questionnaire Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11<br/>2.4.1 Demographic Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11<br/>2.4.2 Technical Questions Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 13<br/>2.5 Key Findings and Implications of Mobile Applications Development in Industry . . 18<br/>VIII<br/>3. LLMs and Transcompilers for Mobile Application Code Translation . . . . . . . . . . . . 20<br/>3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20<br/>3.2 Literature Review on Code Translation . . . . . . . . . . . . . . . . . . . . . . . . . 20<br/>3.2.1 Translation of Mobile Application Code . . . . . . . . . . . . . . . . . . . . 20<br/>3.2.2 LLMs for Code Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . 24<br/>3.3 Case Studies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26<br/>3.3.1 Web Services Code Translation from Swift to Java . . . . . . . . . . . . . . 26<br/>3.3.2 Translating from JavaScript to Swift and Java . . . . . . . . . . . . . . . . . 27<br/>3.3.3 GPT4o Evaluation to Translate from Swift to Java . . . . . . . . . . . . . . 28<br/>3.4 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29<br/>3.4.1 Results of Web Services Code Translation . . . . . . . . . . . . . . . . . . . 29<br/>3.4.2 Results of Translation from JavaScript to Java and Swift . . . . . . . . . . . 29<br/>3.4.3 Results of Evaluating GPT4o . . . . . . . . . . . . . . . . . . . . . . . . . . 31<br/>3.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33<br/>4. Formal Verification Approaches for Code Conversion . . . . . . . . . . . . . . . . . . . . 34<br/>4.1 Background and Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34<br/>4.1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35<br/>4.2 Literature of Previous Reviews of Formal Verification . . . . . . . . . . . . . . . . . 36<br/>4.3 Research Corpus Collection Methodology . . . . . . . . . . . . . . . . . . . . . . . 37<br/>4.3.1 Verification Approaches Categorization Methodology . . . . . . . . . . . . . 39<br/>4.4 Verification Techniques for Code Optimization . . . . . . . . . . . . . . . . . . . . . 40<br/>4.4.1 Symbolic Execution for Equivalence Checking . . . . . . . . . . . . . . . . . 40<br/>4.4.2 Equivalence Checking Using State-Machine Representations . . . . . . . . . 44<br/>4.4.3 Equivalence Checking via Assertions . . . . . . . . . . . . . . . . . . . . . . 49<br/>4.4.4 Proof-Based Verification of Compiler Optimizations . . . . . . . . . . . . . . 50<br/>4.5 Formal Verification of Code-to-Code Translation . . . . . . . . . . . . . . . . . . . 52<br/>4.5.1 Symbolic Execution for Cross-Language Equivalence Checking . . . . . . . . 53<br/>4.5.2 Assertions Based on K-Safety Properties for Translation Verification . . . . 53<br/>4.5.3 Proof-Based Verification of Code Translators . . . . . . . . . . . . . . . . . 53<br/>4.6 Formal Verification of Model-Based Code Generation . . . . . . . . . . . . . . . . . 55<br/>4.6.1 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55<br/>4.6.2 Assertions and Formal Proof Obligations for Equivalence Verification . . . . 56<br/>4.7 Analysis of the Trends in Formal Verification of Code Conversion . . . . . . . . . . 57<br/>4.7.1 State-Machine and Graph-Based Equivalence Checking . . . . . . . . . . . . 61<br/>4.7.2 Proof-Based Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61<br/>4.7.3 Symbolic Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61<br/>4.7.4 Assertion-Based Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 62<br/>4.7.5 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62<br/>4.8 Analysis of Formal Verification Methods for Cross-Language Code Translation . . . 63<br/>4.8.1 Proof-Based Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63<br/>4.8.2 Symbolic Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63<br/>4.8.3 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64<br/>4.8.4 State-Machines and Model-Checking . . . . . . . . . . . . . . . . . . . . . . 64<br/>IX<br/>5. A Model-Checking-Based Verification Approach for Transcompilers . . . . . . . . . . . . 66<br/>5.1 Literature Review on Translators Verification . . . . . . . . . . . . . . . . . . . . . 67<br/>5.2 The TC-Verifier Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68<br/>5.2.1 Transcompiler-Based Code Translators . . . . . . . . . . . . . . . . . . . . . 68<br/>5.2.2 Tool Selection for Model Checking . . . . . . . . . . . . . . . . . . . . . . . 69<br/>5.2.3 Key Components and Concepts in Uppaal . . . . . . . . . . . . . . . . . . . 70<br/>5.2.4 The TC-Verifier Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . 71<br/>5.2.5 Evaluation Metric: Verification Success Rate . . . . . . . . . . . . . . . . . . 73<br/>5.2.6 Applying the Verifier Model to a Translator Case Study . . . . . . . . . . . 74<br/>5.3 Experimental Setup: Statements Modeled . . . . . . . . . . . . . . . . . . . . . . . 77<br/>5.3.1 Variable Declaration Statement . . . . . . . . . . . . . . . . . . . . . . . . . 77<br/>5.3.2 Function Declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78<br/>5.3.3 Class Declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81<br/>5.3.4 While Statement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82<br/>5.4 Results of Applying TC-Verifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84<br/>5.4.1 Variable Declaration Verification . . . . . . . . . . . . . . . . . . . . . . . . 84<br/>5.4.2 Function Declaration Verification . . . . . . . . . . . . . . . . . . . . . . . . 85<br/>5.4.3 Class Declaration Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 87<br/>5.4.4 While Statement Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 88<br/>5.4.5 Comparison with BLEU Score . . . . . . . . . . . . . . . . . . . . . . . . . . 88<br/>5.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90<br/>6. Enhancing LLMs Using TransCompiler-Assisted Prompting . . . . . . . . . . . . . . . . 92<br/>6.1 Literature Review . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93<br/>6.2 Methodology of TC-Assisted Prompting . . . . . . . . . . . . . . . . . . . . . . . . 94<br/>6.3 Case Studies: Selected Models and Experimental Design . . . . . . . . . . . . . . . 95<br/>6.3.1 Models Selection Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96<br/>6.3.2 Two-Step Experimental Setup . . . . . . . . . . . . . . . . . . . . . . . . . . 96<br/>6.3.3 Codestral Fine-tuning Experiment . . . . . . . . . . . . . . . . . . . . . . . 97<br/>6.4 Datasets Used for Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99<br/>6.4.1 New dataset TGAlpaca . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99<br/>6.4.2 HumanEvalX Dataset . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99<br/>6.4.3 XLCoST Dataset . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100<br/>6.4.4 Cyclomatic Complexity of Code CC . . . . . . . . . . . . . . . . . . . . . . 100<br/>6.5 Evaluation Metrics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101<br/>6.5.1 Compilation Success Rate . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101<br/>6.5.2 Assertion-Based Validation . . . . . . . . . . . . . . . . . . . . . . . . . . . 102<br/>6.5.3 pass@1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103<br/>6.5.4 CodeBLEU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103<br/>6.6 Results of LLMs enhancement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103<br/>6.6.1 Results on TGAlpaca dataset . . . . . . . . . . . . . . . . . . . . . . . . . . 103<br/>6.6.2 Comparison Results with HumanEvalX Dataset . . . . . . . . . . . . . . . . 106<br/>6.6.3 Comparison Results with XLCoST Dataset . . . . . . . . . . . . . . . . . . 108<br/>6.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110<br/>6.7.1 TC-Assisted Prompting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110<br/>6.7.2 No More Fine-Tuning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110<br/>6.7.3 Evaluation Metrics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111<br/>6.7.4 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111<br/>X<br/>7. Conclusion and Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113<br/>7.1 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113<br/>7.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114<br/>Appendices:<br/>A. Questionnaire Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115<br/>B. Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117<br/>Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 |
| 520 3# - Abstract |
|---|
| Abstract |
Abstract:<br/>Code translation is a critical task in software engineering, particularly for cross-platform development. Building mobile applications across platforms often requires translation between native<br/>languages such as Java, Swift, and Kotlin. While modern frameworks like React Native and Flutter<br/>have gained traction, translation between cross-platform languages (e.g., JavaScript and Dart) and<br/>native languages remains a practical necessity for developers.<br/>Previous research has proposed transcompiler-based translators for mobile application languages.<br/>However, developers rarely adopt these tools due to their incompleteness and the unquantified nature of their coverage, often lacking rigorous validation or verification. At the same time, large<br/>language models (LLMs) have transformed code generation tasks, including code completion, generation, summarization, and translation, by leveraging large-scale training datasets. Yet, datasets<br/>specifically focused on mobile application languages remain scarce and underexplored.<br/>In this dissertation, we propose transcompiler-assisted prompting of LLMs for code translation.<br/>We begin by introducing a methodology to formally verify both the capabilities and limitations of<br/>existing compiler-based translators. This verification identifies which translation rules are correctly<br/>covered and which are not. The verification process revealed 50.7% coverage for the transcompiler<br/>under study. The verified partial translations produced by the transcompiler, guaranteed to be<br/>correct for the parts they cover, are then embedded into the prompts provided to LLMs. These<br/>verified fragments guide the LLMs toward reduced hallucination and improved syntactic and semantic<br/>correctness in their output.<br/>We apply this prompt-aided methodology to three different LLMs and evaluate their performance<br/>using our newly created dataset, TGAlpaca, including 902 different code snippets, and two benchmark<br/>datasets, HumanEval-X and XlCost. Our results show improvements ranging from 1% to 40% across<br/>all three models for TGAlpaca. Furthermore, benchmark comparisons with the HumanEvalX data<br/>set achieved a pass@1 score comparable to the CodeGeex fine-tuned model and a 21-27 pass@1 score<br/>improvement over other baseline models. This demonstrates that our approach achieves competitive<br/>or superior translation quality while saving computational resources otherwise required for training<br/>or fine-tuning.<br/>Keywords<br/>Code translation, Formal verification, Large language models, Model checking, Mobile Application development<br/> |
| 546 ## - Language Note |
|---|
| Language Note |
Text in English, abstracts in English and Arabic |
| 650 #4 - Subject |
|---|
| Subject |
Software Engineering |
| 655 #7 - Index Term-Genre/Form |
|---|
| Source of term |
NULIB |
| focus term |
Dissertation, Academic |
| 690 ## - Subject |
|---|
| School |
Software Engineering |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Source of classification or shelving scheme |
Dewey Decimal Classification |
| Koha item type |
Thesis |
| 650 #4 - Subject |
|---|
| -- |
211 |
| 655 #7 - Index Term-Genre/Form |
|---|
| -- |
187 |
| 690 ## - Subject |
|---|
| -- |
211 |