# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 1 Introduction  
In modern software engineering, ensuring the reliability of software systems is essential, particularly as software becomes more complex and integrated into critical applications. Formal software verification ensures that a system satisfies predefined formal specifications. These methods are now widely used in the software industry to enhance software reliability and reduce the cost associated with fixing errors during the testing phase of the software life cycle [1]. Instead, errors are eliminated at the design stage in the case of correct-by-construction software. If the system is already implemented, it can be formally verified by theorem proving, model checking, and formal assertions. However, despite the widespread adoption of formal verification techniques in areas like low-level code verification and compiler optimization, there is a significant gap in their application to code translation between high-level languages. Formal verification was used in the compiler verification context to translate high-level code to a lower-level representation or verify compiler optimization. Early work on compiler verification has focused specifically on verifying C/C++ code [2] and LLVM intermediate representations (LLVM IR) [3]. LLVM, in this context, serves as a collection of modular and reusable compiler and toolchain technologies. To the best of the authors' knowledge, almost no previous research applied formal methods for code translation between high-level languages. The Trans-compiler-based high-level code translators mentioned in previous surveys [2, 4], in addition to the recent trans-compilers [5, 6], are evaluated by functional testing or by bilingual evaluation understudy (BLEU) score [7]. Functional testing tests the generated code's functionality and is usually based on benchmarks with a finite number of test cases. The BLEU score is widely used to evaluate machine-translated text versus human translation, which acts as a reference [8]. The higher the BLEU score, the more similar the generated translation is to the reference or ground truth translation. CodeBleu, an enhanced version of BLEU, is calculated similarly to the BLEU metric and involves comparing the n-gram precision of the generated code with the reference code, considering the similarity of the code structures. However, studies have demonstrated that BLEU does not reliably reflect the translation quality for code migration tasks [9]. In addition, code translation also implies the presence of benchmark datasets of parallel code snippets. The available benchmarks include certain languages like C++, C#, Python, and Java. At the same time, there is a scarcity of benchmark datasets for other programming languages [10]. The mentioned evaluation methods have to be applied to the result of each run of the translator, with no guarantee for the correctness and completeness of the code translator. Correctness serves to ensure that the translated code complies with the grammar rules of the destination language and retains the same semantics as the source code. Completeness serves to ensure that all grammar rules of the source languages are fully translated. In this work, we propose \"TC-Verifier\" as a formal verification architecture based on model checking that can be applied to trans-compiler-based code translators, specifically code translators based on parser generators. The modeling can be applied to the translators, whether they are implemented or under design. Model checking serves to represent a system in the form of states and transitions, then apply the verification of certain properties and specifications on the state machine representation [11]. A model checker can exhaustively and systematically explore all the possible behaviors of the state space rather than certain behaviors [12]. We introduce a novel architecture employing the Uppaal model checker to formally verify trans-compiler-based code translators.