TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking

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.